Theorem feqmptd 6902

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5179   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  feqresmpt  6903  cofmpt  7077  fcoconst  7079  ofco  7647  caofinvl  7654  caofcom  7659  caofidlcan  7660  caofass  7662  caofdi  7664  caofdir  7665  caonncan  7666  suppssof1  8141  mapxpen  9071  xpmapenlem  9072  cantnfp1  9590  cantnflem1  9598  cnfcom2lem  9610  infxpenc  9928  pwfseqlem5  10574  gruf  10722  ccatco  14758  cnrecnv  15088  rlimclim1  15468  rlimuni  15473  lo1resb  15487  rlimresb  15488  o1resb  15489  rlimcn1  15511  rlimo1  15540  o1rlimmul  15542  caucvgr  15599  ackbijnn  15751  bitsf1ocnv  16371  ramcl  16957  pwsplusgval  17411  pwsmulrval  17412  pwsvscafval  17415  setcepi  18012  prf1st  18127  prf2nd  18128  1st2ndprf  18129  curfuncf  18161  curf2ndf  18170  yonedainv  18204  yonffthlem  18205  prdsidlem  18694  mhmvlin  18726  pwsco1mhm  18757  pwsco2mhm  18758  frmdup3lem  18791  frmdup3  18792  grpinvcnv  18936  pwsinvg  18983  pwssub  18984  efginvrel1  19657  frgpup3lem  19706  frgpup3  19707  gsumval3  19836  gsumcllem  19837  gsumzf1o  19841  gsumzsplit  19856  gsumconst  19863  gsumzmhm  19866  gsumsub  19877  gsum2dlem2  19900  gsumcom2  19904  dprdfadd  19951  dprdfsub  19952  dprdfeq0  19953  dprdf11  19954  dmdprdsplitlem  19968  dprddisj2  19970  dpjidcl  19989  ablfaclem2  20017  ablfac2  20020  rrgsupp  20634  mptscmfsuppd  20879  lmhmvsca  20997  mulgrhm2  21433  cygznlem2a  21522  frgpcyg  21528  uvcresum  21748  frlmup1  21753  gsumbagdiaglem  21886  psrass1lem  21888  psrlinv  21911  psrass1  21919  psrcom  21923  mplsubrglem  21959  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  evlslem2  22034  evlslem6  22036  evlslem1  22037  mhpmulcl  22092  psdmplcl  22105  psdmul  22109  coe1fval3  22149  coe1sclmul  22224  coe1sclmul2  22226  grpvrinv  22343  mdetleib2  22532  mdetunilem9  22564  cayleyhamilton1  22836  neiptopnei  23076  dfac14  23562  ptcnp  23566  lmcn2  23593  cnmpt11f  23608  cnmpt21f  23616  cnmpt2k  23632  qtopeu  23660  xkocnv  23758  xkohmeo  23759  flfcnp2  23951  istgp2  24035  tmdgsum  24039  subgtgp  24049  symgtgp  24050  tgpconncomp  24057  prdstgpd  24069  tsmssub  24093  tgptsmscls  24094  tsmssplit  24096  tsmsxplem1  24097  tlmtgp  24140  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  25447  ovolfs2  25528  uniioombllem2  25540  ismbf  25585  mbfconst  25590  mbfmulc2re  25605  mbfadd  25618  mbfsub  25619  mbflimsup  25623  mbfi1flimlem  25679  mbfi1flim  25680  mbfmul  25683  itg2uba  25700  itg2mulclem  25703  itg2mulc  25704  itg2splitlem  25705  itg2monolem1  25707  itg2i1fseq  25712  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  i1fibl  25765  itgitg1  25766  bddmulibl  25796  bddiblnc  25799  cnplimc  25844  limccnp2  25849  dvcnp2  25877  dvcnp2OLD  25878  dvmulf  25902  dvcmulf  25904  dvcobr  25905  dvcobrOLD  25906  dvcof  25908  dvcj  25910  dvfre  25911  dvmptcj  25928  dvcnvlem  25936  dvcnv  25937  dvef  25940  dvsincos  25941  rolle  25950  cmvth  25951  cmvthOLD  25952  dvlip  25954  dvlipcn  25955  dv11cn  25962  dvivthlem1  25969  dvivth  25971  lhop2  25976  dvfsumrlim2  25995  ftc1lem1  25998  ftc1lem2  25999  ftc1a  26000  ftc1lem4  26002  ftc2  26007  ftc2ditglem  26008  ftc2ditg  26009  tdeglem4  26021  tdeglem2  26022  mdegle0  26038  mdegmullem  26039  plypf1  26173  plyco  26202  dgrcolem1  26235  dgrcolem2  26236  dgrco  26237  plycjlem  26238  dvply2g  26248  dvply2gOLD  26249  plydiveu  26262  elqaalem3  26285  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmshft  26355  ulmdvlem1  26365  mtest  26369  mtestbdd  26370  mbfulm  26371  iblulm  26372  itgulm  26373  pserulm  26387  pserdv  26395  abelthlem1  26397  abelthlem3  26399  pige3ALT  26485  eff1olem  26513  logcn  26612  advlog  26619  advlogexp  26620  logtayl  26625  logccv  26628  dvcxp1  26705  dvcxp2  26706  dvcncxp1  26708  resqrtcn  26715  sqrtcn  26716  loglesqrt  26727  dvatan  26901  leibpi  26908  divsqrtsumo1  26950  jensenlem2  26954  amgmlem  26956  lgamgulmlem2  26996  ftalem7  27045  basellem9  27055  muinv  27159  dchrmullid  27219  dchrinvcl  27220  dchrisum0lem2a  27484  logdivsum  27500  mulog2sumlem1  27501  log2sumbnd  27511  hilnormi  31238  chscllem4  31715  hmopidmchi  32226  rabfodom  32580  ofoprabco  32742  fpwrelmapffslem  32811  fpwrelmap  32812  prodindf  32944  gsummulsubdishift1  33151  gsumwrd2dccat  33160  elrgspn  33328  elrgspnsubrunlem2  33330  domnprodeq0  33358  deg1prod  33664  mplmulmvr  33704  evlextv  33707  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmrhm  33712  issply  33719  esplyfval0  33722  lbsdiflsp0  33783  fedgmullem1  33786  extdgfialglem2  33850  qqhre  34177  esumpcvgval  34235  ofcfval4  34262  omssubadd  34457  carsggect  34475  plymulx0  34704  fdvneggt  34757  fdvnegge  34759  itgexpif  34763  ptpconn  35427  cvmliftlem6  35484  cvmliftlem8  35486  cvmlift2lem7  35503  cvmliftphtlem  35511  cvmlift3lem5  35517  elmsubrn  35722  knoppcnlem9  36701  curunc  37803  poimir  37854  broucube  37855  mblfinlem2  37859  volsupnfl  37866  cnambfre  37869  dvtan  37871  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  itgaddnc  37881  itgmulc2nc  37889  ftc1cnnclem  37892  ftc1anclem1  37894  ftc1anclem2  37895  ftc1anclem3  37896  ftc1anclem4  37897  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  ftc2nc  37903  upixp  37930  readvcot  42619  selvvvval  42828  evlselv  42830  fsuppssindlem1  42834  fsuppssindlem2  42835  mhphflem  42839  mhphf  42840  mzpsubst  42990  diophun  43015  mendlmod  43431  mendassa  43432  cantnf2  43567  fsovcnvlem  44254  binomcxplemnotnn0  44597  rnsnf  45428  cncfmptss  45833  climliminflimsupd  46045  mulcncff  46114  subcncff  46124  cncfcompt  46127  addcncff  46128  divcncff  46135  cncfiooicclem1  46137  dvsinexp  46155  dvsubf  46158  dvdivf  46166  dvcosax  46170  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  itgsinexplem1  46198  itgsubsticclem  46219  iblcncfioo  46222  itgiccshift  46224  stoweidlem20  46264  dirkercncflem2  46348  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem28  46379  fourierdlem39  46390  fourierdlem51  46401  fourierdlem60  46410  fourierdlem61  46411  fourierdlem69  46419  fourierdlem72  46422  fourierdlem73  46423  fourierdlem81  46431  fourierdlem83  46433  fourierdlem84  46434  fourierdlem87  46437  fourierdlem90  46440  fourierdlem93  46443  fourierdlem95  46445  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  etransclem34  46512  etransclem43  46521  etransclem46  46524  sge0tsms  46624  sge0fodjrnlem  46660  sge0iun  46663  sge0isum  46671  sge0seq  46690  meadjun  46706  meadjiunlem  46709  meadjiun  46710  ismeannd  46711  psmeasurelem  46714  omeiunle  46761  ovn02  46812  smfpimioo  47031  smfresal  47032  smfinflem  47061  smflimsuplem3  47066  smfliminflem  47074  1arymaptfo  48889  diag1  49549  aacllem  50046  amgmwlem  50047  amgmlemALT  50048