Theorem feqmptd 6929

Description: Deduction form of dffn5 6919. (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 6689	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		dffn5 6919	. 2 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
4	2, 3	sylib 218	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5188   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  feqresmpt  6930  cofmpt  7104  fcoconst  7106  ofco  7678  caofinvl  7685  caofcom  7690  caofidlcan  7691  caofass  7693  caofdi  7695  caofdir  7696  caonncan  7697  suppssof1  8178  mapxpen  9107  xpmapenlem  9108  cantnfp1  9634  cantnflem1  9642  cnfcom2lem  9654  infxpenc  9971  pwfseqlem5  10616  gruf  10764  ccatco  14801  cnrecnv  15131  rlimclim1  15511  rlimuni  15516  lo1resb  15530  rlimresb  15531  o1resb  15532  rlimcn1  15554  rlimo1  15583  o1rlimmul  15585  caucvgr  15642  ackbijnn  15794  bitsf1ocnv  16414  ramcl  17000  pwsplusgval  17453  pwsmulrval  17454  pwsvscafval  17457  setcepi  18050  prf1st  18165  prf2nd  18166  1st2ndprf  18167  curfuncf  18199  curf2ndf  18208  yonedainv  18242  yonffthlem  18243  prdsidlem  18696  mhmvlin  18728  pwsco1mhm  18759  pwsco2mhm  18760  frmdup3lem  18793  frmdup3  18794  grpinvcnv  18938  pwsinvg  18985  pwssub  18986  efginvrel1  19658  frgpup3lem  19707  frgpup3  19708  gsumval3  19837  gsumcllem  19838  gsumzf1o  19842  gsumzsplit  19857  gsumconst  19864  gsumzmhm  19867  gsumsub  19878  gsum2dlem2  19901  gsumcom2  19905  dprdfadd  19952  dprdfsub  19953  dprdfeq0  19954  dprdf11  19955  dmdprdsplitlem  19969  dprddisj2  19971  dpjidcl  19990  ablfaclem2  20018  ablfac2  20021  rrgsupp  20610  mptscmfsuppd  20834  lmhmvsca  20952  mulgrhm2  21388  cygznlem2a  21477  frgpcyg  21483  uvcresum  21702  frlmup1  21707  gsumbagdiaglem  21839  psrass1lem  21841  psrlinv  21864  psrass1  21873  psrcom  21877  mplsubrglem  21913  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  evlslem2  21986  evlslem6  21988  evlslem1  21989  mhpmulcl  22036  psdmplcl  22049  psdmul  22053  coe1fval3  22093  coe1sclmul  22168  coe1sclmul2  22170  grpvrinv  22286  mdetleib2  22475  mdetunilem9  22507  cayleyhamilton1  22779  neiptopnei  23019  dfac14  23505  ptcnp  23509  lmcn2  23536  cnmpt11f  23551  cnmpt21f  23559  cnmpt2k  23575  qtopeu  23603  xkocnv  23701  xkohmeo  23702  flfcnp2  23894  istgp2  23978  tmdgsum  23982  subgtgp  23992  symgtgp  23993  tgpconncomp  24000  prdstgpd  24012  tsmssub  24036  tgptsmscls  24037  tsmssplit  24039  tsmsxplem1  24040  tlmtgp  24083  ustuqtop  24134  prdsmslem1  24415  prdsxmslem1  24416  prdsxmslem2  24417  tngnm  24539  nmoeq0  24624  cnfldnm  24666  cncfmpt1f  24807  negfcncf  24817  cnrehmeo  24851  cnrehmeoOLD  24852  evth  24858  evth2  24859  copco  24918  pcopt  24922  pcopt2  24923  pcoass  24924  pcorev2  24928  pi1xfrcnv  24957  ovolctb  25391  ovolfs2  25472  uniioombllem2  25484  ismbf  25529  mbfconst  25534  mbfmulc2re  25549  mbfadd  25562  mbfsub  25563  mbflimsup  25567  mbfi1flimlem  25623  mbfi1flim  25624  mbfmul  25627  itg2uba  25644  itg2mulclem  25647  itg2mulc  25648  itg2splitlem  25649  itg2monolem1  25651  itg2i1fseq  25656  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  i1fibl  25709  itgitg1  25710  bddmulibl  25740  bddiblnc  25743  cnplimc  25788  limccnp2  25793  dvcnp2  25821  dvcnp2OLD  25822  dvmulf  25846  dvcmulf  25848  dvcobr  25849  dvcobrOLD  25850  dvcof  25852  dvcj  25854  dvfre  25855  dvmptcj  25872  dvcnvlem  25880  dvcnv  25881  dvef  25884  dvsincos  25885  rolle  25894  cmvth  25895  cmvthOLD  25896  dvlip  25898  dvlipcn  25899  dv11cn  25906  dvivthlem1  25913  dvivth  25915  lhop2  25920  dvfsumrlim2  25939  ftc1lem1  25942  ftc1lem2  25943  ftc1a  25944  ftc1lem4  25946  ftc2  25951  ftc2ditglem  25952  ftc2ditg  25953  tdeglem4  25965  tdeglem2  25966  mdegle0  25982  mdegmullem  25983  plypf1  26117  plyco  26146  dgrcolem1  26179  dgrcolem2  26180  dgrco  26181  plycjlem  26182  dvply2g  26192  dvply2gOLD  26193  plydiveu  26206  elqaalem3  26229  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmshft  26299  ulmdvlem1  26309  mtest  26313  mtestbdd  26314  mbfulm  26315  iblulm  26316  itgulm  26317  pserulm  26331  pserdv  26339  abelthlem1  26341  abelthlem3  26343  pige3ALT  26429  eff1olem  26457  logcn  26556  advlog  26563  advlogexp  26564  logtayl  26569  logccv  26572  dvcxp1  26649  dvcxp2  26650  dvcncxp1  26652  resqrtcn  26659  sqrtcn  26660  loglesqrt  26671  dvatan  26845  leibpi  26852  divsqrtsumo1  26894  jensenlem2  26898  amgmlem  26900  lgamgulmlem2  26940  ftalem7  26989  basellem9  26999  muinv  27103  dchrmullid  27163  dchrinvcl  27164  dchrisum0lem2a  27428  logdivsum  27444  mulog2sumlem1  27445  log2sumbnd  27455  hilnormi  31092  chscllem4  31569  hmopidmchi  32080  rabfodom  32434  ofoprabco  32588  fpwrelmapffslem  32655  fpwrelmap  32656  prodindf  32786  gsumwrd2dccat  33007  elrgspn  33197  elrgspnsubrunlem2  33199  lbsdiflsp0  33622  fedgmullem1  33625  qqhre  34010  esumpcvgval  34068  ofcfval4  34095  omssubadd  34291  carsggect  34309  plymulx0  34538  fdvneggt  34591  fdvnegge  34593  itgexpif  34597  ptpconn  35220  cvmliftlem6  35277  cvmliftlem8  35279  cvmlift2lem7  35296  cvmliftphtlem  35304  cvmlift3lem5  35310  elmsubrn  35515  knoppcnlem9  36489  curunc  37596  poimir  37647  broucube  37648  mblfinlem2  37652  volsupnfl  37659  cnambfre  37662  dvtan  37664  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  itgaddnc  37674  itgmulc2nc  37682  ftc1cnnclem  37685  ftc1anclem1  37687  ftc1anclem2  37688  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  upixp  37723  readvcot  42352  selvvvval  42573  evlselv  42575  fsuppssindlem1  42579  fsuppssindlem2  42580  mhphflem  42584  mhphf  42585  mzpsubst  42736  diophun  42761  mendlmod  43178  mendassa  43179  cantnf2  43314  fsovcnvlem  44002  binomcxplemnotnn0  44345  rnsnf  45178  cncfmptss  45585  climliminflimsupd  45799  mulcncff  45868  subcncff  45878  cncfcompt  45881  addcncff  45882  divcncff  45889  cncfiooicclem1  45891  dvsinexp  45909  dvsubf  45912  dvdivf  45920  dvcosax  45924  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  itgsinexplem1  45952  itgsubsticclem  45973  iblcncfioo  45976  itgiccshift  45978  stoweidlem20  46018  dirkercncflem2  46102  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem28  46133  fourierdlem39  46144  fourierdlem51  46155  fourierdlem60  46164  fourierdlem61  46165  fourierdlem69  46173  fourierdlem72  46176  fourierdlem73  46177  fourierdlem81  46185  fourierdlem83  46187  fourierdlem84  46188  fourierdlem87  46191  fourierdlem90  46194  fourierdlem93  46197  fourierdlem95  46199  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  etransclem34  46266  etransclem43  46275  etransclem46  46278  sge0tsms  46378  sge0fodjrnlem  46414  sge0iun  46417  sge0isum  46425  sge0seq  46444  meadjun  46460  meadjiunlem  46463  meadjiun  46464  ismeannd  46465  psmeasurelem  46468  omeiunle  46515  ovn02  46566  smfpimioo  46785  smfresal  46786  smfinflem  46815  smflimsuplem3  46820  smfliminflem  46828  1arymaptfo  48632  diag1  49293  aacllem  49790  amgmwlem  49791  amgmlemALT  49792