Theorem feqmptd 6952

Description: Deduction form of dffn5 6942. (Contributed by Mario Carneiro, 8-Jan-2015.)

Hypothesis

Ref	Expression
feqmptd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
feqmptd	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem feqmptd

Step	Hyp	Ref	Expression
1		feqmptd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6712	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		dffn5 6942	. 2 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
4	2, 3	sylib 218	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5206   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  feqresmpt  6953  cofmpt  7127  fcoconst  7129  ofco  7701  caofinvl  7708  caofcom  7713  caofidlcan  7714  caofass  7716  caofdi  7718  caofdir  7719  caonncan  7720  suppssof1  8203  mapxpen  9162  xpmapenlem  9163  cantnfp1  9700  cantnflem1  9708  cnfcom2lem  9720  infxpenc  10037  pwfseqlem5  10682  gruf  10830  ccatco  14859  cnrecnv  15189  rlimclim1  15566  rlimuni  15571  lo1resb  15585  rlimresb  15586  o1resb  15587  rlimcn1  15609  rlimo1  15638  o1rlimmul  15640  caucvgr  15697  ackbijnn  15849  bitsf1ocnv  16468  ramcl  17054  pwsplusgval  17509  pwsmulrval  17510  pwsvscafval  17513  setcepi  18106  prf1st  18221  prf2nd  18222  1st2ndprf  18223  curfuncf  18255  curf2ndf  18264  yonedainv  18298  yonffthlem  18299  prdsidlem  18752  mhmvlin  18784  pwsco1mhm  18815  pwsco2mhm  18816  frmdup3lem  18849  frmdup3  18850  grpinvcnv  18994  pwsinvg  19041  pwssub  19042  efginvrel1  19714  frgpup3lem  19763  frgpup3  19764  gsumval3  19893  gsumcllem  19894  gsumzf1o  19898  gsumzsplit  19913  gsumconst  19920  gsumzmhm  19923  gsumsub  19934  gsum2dlem2  19957  gsumcom2  19961  dprdfadd  20008  dprdfsub  20009  dprdfeq0  20010  dprdf11  20011  dmdprdsplitlem  20025  dprddisj2  20027  dpjidcl  20046  ablfaclem2  20074  ablfac2  20077  rrgsupp  20666  mptscmfsuppd  20890  lmhmvsca  21008  mulgrhm2  21444  cygznlem2a  21533  frgpcyg  21539  uvcresum  21758  frlmup1  21763  gsumbagdiaglem  21895  psrass1lem  21897  psrlinv  21920  psrass1  21929  psrcom  21933  mplsubrglem  21969  mplmonmul  21999  mplcoe1  22000  mplcoe5  22003  evlslem2  22042  evlslem6  22044  evlslem1  22045  mhpmulcl  22092  psdmplcl  22105  psdmul  22109  coe1fval3  22149  coe1sclmul  22224  coe1sclmul2  22226  grpvrinv  22342  mdetleib2  22531  mdetunilem9  22563  cayleyhamilton1  22835  neiptopnei  23075  dfac14  23561  ptcnp  23565  lmcn2  23592  cnmpt11f  23607  cnmpt21f  23615  cnmpt2k  23631  qtopeu  23659  xkocnv  23757  xkohmeo  23758  flfcnp2  23950  istgp2  24034  tmdgsum  24038  subgtgp  24048  symgtgp  24049  tgpconncomp  24056  prdstgpd  24068  tsmssub  24092  tgptsmscls  24093  tsmssplit  24095  tsmsxplem1  24096  tlmtgp  24139  ustuqtop  24190  prdsmslem1  24471  prdsxmslem1  24472  prdsxmslem2  24473  tngnm  24595  nmoeq0  24680  cnfldnm  24722  cncfmpt1f  24863  negfcncf  24873  cnrehmeo  24907  cnrehmeoOLD  24908  evth  24914  evth2  24915  copco  24974  pcopt  24978  pcopt2  24979  pcoass  24980  pcorev2  24984  pi1xfrcnv  25013  ovolctb  25448  ovolfs2  25529  uniioombllem2  25541  ismbf  25586  mbfconst  25591  mbfmulc2re  25606  mbfadd  25619  mbfsub  25620  mbflimsup  25624  mbfi1flimlem  25680  mbfi1flim  25681  mbfmul  25684  itg2uba  25701  itg2mulclem  25704  itg2mulc  25705  itg2splitlem  25706  itg2monolem1  25708  itg2i1fseq  25713  itg2gt0  25718  itg2cnlem1  25719  itg2cnlem2  25720  i1fibl  25766  itgitg1  25767  bddmulibl  25797  bddiblnc  25800  cnplimc  25845  limccnp2  25850  dvcnp2  25878  dvcnp2OLD  25879  dvmulf  25903  dvcmulf  25905  dvcobr  25906  dvcobrOLD  25907  dvcof  25909  dvcj  25911  dvfre  25912  dvmptcj  25929  dvcnvlem  25937  dvcnv  25938  dvef  25941  dvsincos  25942  rolle  25951  cmvth  25952  cmvthOLD  25953  dvlip  25955  dvlipcn  25956  dv11cn  25963  dvivthlem1  25970  dvivth  25972  lhop2  25977  dvfsumrlim2  25996  ftc1lem1  25999  ftc1lem2  26000  ftc1a  26001  ftc1lem4  26003  ftc2  26008  ftc2ditglem  26009  ftc2ditg  26010  tdeglem4  26022  tdeglem2  26023  mdegle0  26039  mdegmullem  26040  plypf1  26174  plyco  26203  dgrcolem1  26236  dgrcolem2  26237  dgrco  26238  plycjlem  26239  dvply2g  26249  dvply2gOLD  26250  plydiveu  26263  elqaalem3  26286  taylthlem1  26338  taylthlem2  26339  taylthlem2OLD  26340  ulmshft  26356  ulmdvlem1  26366  mtest  26370  mtestbdd  26371  mbfulm  26372  iblulm  26373  itgulm  26374  pserulm  26388  pserdv  26396  abelthlem1  26398  abelthlem3  26400  pige3ALT  26486  eff1olem  26514  logcn  26613  advlog  26620  advlogexp  26621  logtayl  26626  logccv  26629  dvcxp1  26706  dvcxp2  26707  dvcncxp1  26709  resqrtcn  26716  sqrtcn  26717  loglesqrt  26728  dvatan  26902  leibpi  26909  divsqrtsumo1  26951  jensenlem2  26955  amgmlem  26957  lgamgulmlem2  26997  ftalem7  27046  basellem9  27056  muinv  27160  dchrmullid  27220  dchrinvcl  27221  dchrisum0lem2a  27485  logdivsum  27501  mulog2sumlem1  27502  log2sumbnd  27512  hilnormi  31149  chscllem4  31626  hmopidmchi  32137  rabfodom  32491  ofoprabco  32647  fpwrelmapffslem  32714  fpwrelmap  32715  prodindf  32845  gsumwrd2dccat  33066  elrgspn  33246  elrgspnsubrunlem2  33248  lbsdiflsp0  33671  fedgmullem1  33674  qqhre  34056  esumpcvgval  34114  ofcfval4  34141  omssubadd  34337  carsggect  34355  plymulx0  34584  fdvneggt  34637  fdvnegge  34639  itgexpif  34643  ptpconn  35260  cvmliftlem6  35317  cvmliftlem8  35319  cvmlift2lem7  35336  cvmliftphtlem  35344  cvmlift3lem5  35350  elmsubrn  35555  knoppcnlem9  36524  curunc  37631  poimir  37682  broucube  37683  mblfinlem2  37687  volsupnfl  37694  cnambfre  37697  dvtan  37699  itg2addnclem  37700  itg2addnclem2  37701  itg2addnclem3  37702  itg2addnc  37703  itg2gt0cn  37704  itgaddnc  37709  itgmulc2nc  37717  ftc1cnnclem  37720  ftc1anclem1  37722  ftc1anclem2  37723  ftc1anclem3  37724  ftc1anclem4  37725  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  ftc2nc  37731  upixp  37758  readvcot  42382  selvvvval  42583  evlselv  42585  fsuppssindlem1  42589  fsuppssindlem2  42590  mhphflem  42594  mhphf  42595  mzpsubst  42746  diophun  42771  mendlmod  43188  mendassa  43189  cantnf2  43324  fsovcnvlem  44012  binomcxplemnotnn0  44355  rnsnf  45188  cncfmptss  45596  climliminflimsupd  45810  mulcncff  45879  subcncff  45889  cncfcompt  45892  addcncff  45893  divcncff  45900  cncfiooicclem1  45902  dvsinexp  45920  dvsubf  45923  dvdivf  45931  dvcosax  45935  dvnmul  45952  dvnprodlem1  45955  dvnprodlem2  45956  itgsinexplem1  45963  itgsubsticclem  45984  iblcncfioo  45987  itgiccshift  45989  stoweidlem20  46029  dirkercncflem2  46113  fourierdlem16  46132  fourierdlem21  46137  fourierdlem22  46138  fourierdlem28  46144  fourierdlem39  46155  fourierdlem51  46166  fourierdlem60  46175  fourierdlem61  46176  fourierdlem69  46184  fourierdlem72  46187  fourierdlem73  46188  fourierdlem81  46196  fourierdlem83  46198  fourierdlem84  46199  fourierdlem87  46202  fourierdlem90  46205  fourierdlem93  46208  fourierdlem95  46210  fourierdlem101  46216  fourierdlem103  46218  fourierdlem104  46219  fourierdlem111  46226  etransclem34  46277  etransclem43  46286  etransclem46  46289  sge0tsms  46389  sge0fodjrnlem  46425  sge0iun  46428  sge0isum  46436  sge0seq  46455  meadjun  46471  meadjiunlem  46474  meadjiun  46475  ismeannd  46476  psmeasurelem  46479  omeiunle  46526  ovn02  46577  smfpimioo  46796  smfresal  46797  smfinflem  46826  smflimsuplem3  46831  smfliminflem  46839  1arymaptfo  48603  diag1  49195  aacllem  49645  amgmwlem  49646  amgmlemALT  49647