Theorem feqmptd 6911

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5183   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507

This theorem is referenced by:  feqresmpt  6912  cofmpt  7086  fcoconst  7088  ofco  7658  caofinvl  7665  caofcom  7670  caofidlcan  7671  caofass  7673  caofdi  7675  caofdir  7676  caonncan  7677  suppssof1  8155  mapxpen  9084  xpmapenlem  9085  cantnfp1  9610  cantnflem1  9618  cnfcom2lem  9630  infxpenc  9947  pwfseqlem5  10592  gruf  10740  ccatco  14777  cnrecnv  15107  rlimclim1  15487  rlimuni  15492  lo1resb  15506  rlimresb  15507  o1resb  15508  rlimcn1  15530  rlimo1  15559  o1rlimmul  15561  caucvgr  15618  ackbijnn  15770  bitsf1ocnv  16390  ramcl  16976  pwsplusgval  17429  pwsmulrval  17430  pwsvscafval  17433  setcepi  18026  prf1st  18141  prf2nd  18142  1st2ndprf  18143  curfuncf  18175  curf2ndf  18184  yonedainv  18218  yonffthlem  18219  prdsidlem  18672  mhmvlin  18704  pwsco1mhm  18735  pwsco2mhm  18736  frmdup3lem  18769  frmdup3  18770  grpinvcnv  18914  pwsinvg  18961  pwssub  18962  efginvrel1  19634  frgpup3lem  19683  frgpup3  19684  gsumval3  19813  gsumcllem  19814  gsumzf1o  19818  gsumzsplit  19833  gsumconst  19840  gsumzmhm  19843  gsumsub  19854  gsum2dlem2  19877  gsumcom2  19881  dprdfadd  19928  dprdfsub  19929  dprdfeq0  19930  dprdf11  19931  dmdprdsplitlem  19945  dprddisj2  19947  dpjidcl  19966  ablfaclem2  19994  ablfac2  19997  rrgsupp  20586  mptscmfsuppd  20810  lmhmvsca  20928  mulgrhm2  21364  cygznlem2a  21453  frgpcyg  21459  uvcresum  21678  frlmup1  21683  gsumbagdiaglem  21815  psrass1lem  21817  psrlinv  21840  psrass1  21849  psrcom  21853  mplsubrglem  21889  mplmonmul  21919  mplcoe1  21920  mplcoe5  21923  evlslem2  21962  evlslem6  21964  evlslem1  21965  mhpmulcl  22012  psdmplcl  22025  psdmul  22029  coe1fval3  22069  coe1sclmul  22144  coe1sclmul2  22146  grpvrinv  22262  mdetleib2  22451  mdetunilem9  22483  cayleyhamilton1  22755  neiptopnei  22995  dfac14  23481  ptcnp  23485  lmcn2  23512  cnmpt11f  23527  cnmpt21f  23535  cnmpt2k  23551  qtopeu  23579  xkocnv  23677  xkohmeo  23678  flfcnp2  23870  istgp2  23954  tmdgsum  23958  subgtgp  23968  symgtgp  23969  tgpconncomp  23976  prdstgpd  23988  tsmssub  24012  tgptsmscls  24013  tsmssplit  24015  tsmsxplem1  24016  tlmtgp  24059  ustuqtop  24110  prdsmslem1  24391  prdsxmslem1  24392  prdsxmslem2  24393  tngnm  24515  nmoeq0  24600  cnfldnm  24642  cncfmpt1f  24783  negfcncf  24793  cnrehmeo  24827  cnrehmeoOLD  24828  evth  24834  evth2  24835  copco  24894  pcopt  24898  pcopt2  24899  pcoass  24900  pcorev2  24904  pi1xfrcnv  24933  ovolctb  25367  ovolfs2  25448  uniioombllem2  25460  ismbf  25505  mbfconst  25510  mbfmulc2re  25525  mbfadd  25538  mbfsub  25539  mbflimsup  25543  mbfi1flimlem  25599  mbfi1flim  25600  mbfmul  25603  itg2uba  25620  itg2mulclem  25623  itg2mulc  25624  itg2splitlem  25625  itg2monolem1  25627  itg2i1fseq  25632  itg2gt0  25637  itg2cnlem1  25638  itg2cnlem2  25639  i1fibl  25685  itgitg1  25686  bddmulibl  25716  bddiblnc  25719  cnplimc  25764  limccnp2  25769  dvcnp2  25797  dvcnp2OLD  25798  dvmulf  25822  dvcmulf  25824  dvcobr  25825  dvcobrOLD  25826  dvcof  25828  dvcj  25830  dvfre  25831  dvmptcj  25848  dvcnvlem  25856  dvcnv  25857  dvef  25860  dvsincos  25861  rolle  25870  cmvth  25871  cmvthOLD  25872  dvlip  25874  dvlipcn  25875  dv11cn  25882  dvivthlem1  25889  dvivth  25891  lhop2  25896  dvfsumrlim2  25915  ftc1lem1  25918  ftc1lem2  25919  ftc1a  25920  ftc1lem4  25922  ftc2  25927  ftc2ditglem  25928  ftc2ditg  25929  tdeglem4  25941  tdeglem2  25942  mdegle0  25958  mdegmullem  25959  plypf1  26093  plyco  26122  dgrcolem1  26155  dgrcolem2  26156  dgrco  26157  plycjlem  26158  dvply2g  26168  dvply2gOLD  26169  plydiveu  26182  elqaalem3  26205  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  ulmshft  26275  ulmdvlem1  26285  mtest  26289  mtestbdd  26290  mbfulm  26291  iblulm  26292  itgulm  26293  pserulm  26307  pserdv  26315  abelthlem1  26317  abelthlem3  26319  pige3ALT  26405  eff1olem  26433  logcn  26532  advlog  26539  advlogexp  26540  logtayl  26545  logccv  26548  dvcxp1  26625  dvcxp2  26626  dvcncxp1  26628  resqrtcn  26635  sqrtcn  26636  loglesqrt  26647  dvatan  26821  leibpi  26828  divsqrtsumo1  26870  jensenlem2  26874  amgmlem  26876  lgamgulmlem2  26916  ftalem7  26965  basellem9  26975  muinv  27079  dchrmullid  27139  dchrinvcl  27140  dchrisum0lem2a  27404  logdivsum  27420  mulog2sumlem1  27421  log2sumbnd  27431  hilnormi  31065  chscllem4  31542  hmopidmchi  32053  rabfodom  32407  ofoprabco  32561  fpwrelmapffslem  32628  fpwrelmap  32629  prodindf  32759  gsumwrd2dccat  32980  elrgspn  33170  elrgspnsubrunlem2  33172  lbsdiflsp0  33595  fedgmullem1  33598  qqhre  33983  esumpcvgval  34041  ofcfval4  34068  omssubadd  34264  carsggect  34282  plymulx0  34511  fdvneggt  34564  fdvnegge  34566  itgexpif  34570  ptpconn  35193  cvmliftlem6  35250  cvmliftlem8  35252  cvmlift2lem7  35269  cvmliftphtlem  35277  cvmlift3lem5  35283  elmsubrn  35488  knoppcnlem9  36462  curunc  37569  poimir  37620  broucube  37621  mblfinlem2  37625  volsupnfl  37632  cnambfre  37635  dvtan  37637  itg2addnclem  37638  itg2addnclem2  37639  itg2addnclem3  37640  itg2addnc  37641  itg2gt0cn  37642  itgaddnc  37647  itgmulc2nc  37655  ftc1cnnclem  37658  ftc1anclem1  37660  ftc1anclem2  37661  ftc1anclem3  37662  ftc1anclem4  37663  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  ftc2nc  37669  upixp  37696  readvcot  42325  selvvvval  42546  evlselv  42548  fsuppssindlem1  42552  fsuppssindlem2  42553  mhphflem  42557  mhphf  42558  mzpsubst  42709  diophun  42734  mendlmod  43151  mendassa  43152  cantnf2  43287  fsovcnvlem  43975  binomcxplemnotnn0  44318  rnsnf  45151  cncfmptss  45558  climliminflimsupd  45772  mulcncff  45841  subcncff  45851  cncfcompt  45854  addcncff  45855  divcncff  45862  cncfiooicclem1  45864  dvsinexp  45882  dvsubf  45885  dvdivf  45893  dvcosax  45897  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  itgsinexplem1  45925  itgsubsticclem  45946  iblcncfioo  45949  itgiccshift  45951  stoweidlem20  45991  dirkercncflem2  46075  fourierdlem16  46094  fourierdlem21  46099  fourierdlem22  46100  fourierdlem28  46106  fourierdlem39  46117  fourierdlem51  46128  fourierdlem60  46137  fourierdlem61  46138  fourierdlem69  46146  fourierdlem72  46149  fourierdlem73  46150  fourierdlem81  46158  fourierdlem83  46160  fourierdlem84  46161  fourierdlem87  46164  fourierdlem90  46167  fourierdlem93  46170  fourierdlem95  46172  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  etransclem34  46239  etransclem43  46248  etransclem46  46251  sge0tsms  46351  sge0fodjrnlem  46387  sge0iun  46390  sge0isum  46398  sge0seq  46417  meadjun  46433  meadjiunlem  46436  meadjiun  46437  ismeannd  46438  psmeasurelem  46441  omeiunle  46488  ovn02  46539  smfpimioo  46758  smfresal  46759  smfinflem  46788  smflimsuplem3  46793  smfliminflem  46801  1arymaptfo  48605  diag1  49266  aacllem  49763  amgmwlem  49764  amgmlemALT  49765