Theorem feqmptd 6708

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

Syntax hints:   → wi 4   = wceq 1538   ↦ cmpt 5110   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332

This theorem is referenced by:  feqresmpt  6709  cofmpt  6871  fcoconst  6873  ofco  7409  caofinvl  7416  caofcom  7421  caofass  7423  caofdi  7425  caofdir  7426  caonncan  7427  suppssof1  7846  mapxpen  8667  xpmapenlem  8668  cantnfp1  9128  cantnflem1  9136  cnfcom2lem  9148  infxpenc  9429  pwfseqlem5  10074  gruf  10222  ccatco  14188  cnrecnv  14516  rlimclim1  14894  rlimuni  14899  lo1resb  14913  rlimresb  14914  o1resb  14915  rlimcn1  14937  rlimo1  14965  o1rlimmul  14967  caucvgr  15024  ackbijnn  15175  bitsf1ocnv  15783  ramcl  16355  pwsplusgval  16755  pwsmulrval  16756  pwsvscafval  16759  setcepi  17340  prf1st  17446  prf2nd  17447  1st2ndprf  17448  curfuncf  17480  curf2ndf  17489  yonedainv  17523  yonffthlem  17524  prdsidlem  17935  pwsco1mhm  17988  pwsco2mhm  17989  frmdup3lem  18023  frmdup3  18024  grpinvcnv  18159  pwsinvg  18204  pwssub  18205  efginvrel1  18846  frgpup3lem  18895  frgpup3  18896  gsumval3  19020  gsumcllem  19021  gsumzf1o  19025  gsumzsplit  19040  gsumconst  19047  gsumzmhm  19050  gsumsub  19061  gsum2dlem2  19084  gsumcom2  19088  dprdfadd  19135  dprdfsub  19136  dprdfeq0  19137  dprdf11  19138  dmdprdsplitlem  19152  dprddisj2  19154  dpjidcl  19173  ablfaclem2  19201  ablfac2  19204  mptscmfsuppd  19693  lmhmvsca  19810  rrgsupp  20057  mulgrhm2  20192  cygznlem2a  20259  frgpcyg  20265  uvcresum  20482  frlmup1  20487  psrbagaddcl  20608  gsumbagdiaglem  20613  psrass1lem  20615  psrlinv  20635  psrass1  20643  psrcom  20647  mplsubrglem  20677  mplmonmul  20704  mplcoe1  20705  mplcoe5  20708  evlslem2  20751  evlslem6  20753  evlslem1  20754  coe1fval3  20837  coe1sclmul  20911  coe1sclmul2  20913  grpvrinv  21003  mhmvlin  21004  mdetleib2  21193  mdetunilem9  21225  cayleyhamilton1  21497  neiptopnei  21737  dfac14  22223  ptcnp  22227  lmcn2  22254  cnmpt11f  22269  cnmpt21f  22277  cnmpt2k  22293  qtopeu  22321  xkocnv  22419  xkohmeo  22420  flfcnp2  22612  istgp2  22696  tmdgsum  22700  subgtgp  22710  symgtgp  22711  tgpconncomp  22718  prdstgpd  22730  tsmssub  22754  tgptsmscls  22755  tsmssplit  22757  tsmsxplem1  22758  tlmtgp  22801  ustuqtop  22852  prdsmslem1  23134  prdsxmslem1  23135  prdsxmslem2  23136  tngnm  23257  nmoeq0  23342  cnfldnm  23384  cncfmpt1f  23519  negfcncf  23528  cnrehmeo  23558  evth  23564  evth2  23565  copco  23623  pcopt  23627  pcopt2  23628  pcoass  23629  pcorev2  23633  pi1xfrcnv  23662  ovolctb  24094  ovolfs2  24175  uniioombllem2  24187  ismbf  24232  mbfconst  24237  mbfmulc2re  24252  mbfadd  24265  mbfsub  24266  mbflimsup  24270  mbfi1flimlem  24326  mbfi1flim  24327  mbfmul  24330  itg2uba  24347  itg2mulclem  24350  itg2mulc  24351  itg2splitlem  24352  itg2monolem1  24354  itg2i1fseq  24359  itg2gt0  24364  itg2cnlem1  24365  itg2cnlem2  24366  i1fibl  24411  itgitg1  24412  bddmulibl  24442  bddiblnc  24445  cnplimc  24490  limccnp2  24495  dvcnp2  24523  dvmulf  24546  dvcmulf  24548  dvcobr  24549  dvcof  24551  dvcj  24553  dvfre  24554  dvmptcj  24571  dvcnvlem  24579  dvcnv  24580  dvef  24583  dvsincos  24584  rolle  24593  cmvth  24594  dvlip  24596  dvlipcn  24597  dv11cn  24604  dvivthlem1  24611  dvivth  24613  lhop2  24618  dvfsumrlim2  24635  ftc1lem1  24638  ftc1lem2  24639  ftc1a  24640  ftc1lem4  24642  ftc2  24647  ftc2ditglem  24648  ftc2ditg  24649  tdeglem4  24661  tdeglem2  24662  mdegle0  24678  mdegmullem  24679  plypf1  24809  plyco  24838  dgrcolem1  24870  dgrcolem2  24871  dgrco  24872  plycjlem  24873  dvply2g  24881  plydiveu  24894  elqaalem3  24917  taylthlem1  24968  taylthlem2  24969  ulmshft  24985  ulmdvlem1  24995  mtest  24999  mtestbdd  25000  mbfulm  25001  iblulm  25002  itgulm  25003  pserulm  25017  pserdv  25024  abelthlem1  25026  abelthlem3  25028  pige3ALT  25112  eff1olem  25140  logcn  25238  advlog  25245  advlogexp  25246  logtayl  25251  logccv  25254  dvcxp1  25329  dvcxp2  25330  dvcncxp1  25332  resqrtcn  25338  sqrtcn  25339  loglesqrt  25347  dvatan  25521  leibpi  25528  divsqrtsumo1  25569  jensenlem2  25573  amgmlem  25575  lgamgulmlem2  25615  ftalem7  25664  basellem9  25674  muinv  25778  dchrmulid2  25836  dchrinvcl  25837  dchrisum0lem2a  26101  logdivsum  26117  mulog2sumlem1  26118  log2sumbnd  26128  hilnormi  28946  chscllem4  29423  hmopidmchi  29934  rabfodom  30274  ofoprabco  30427  fpwrelmapffslem  30494  fpwrelmap  30495  lbsdiflsp0  31110  fedgmullem1  31113  qqhre  31371  prodindf  31392  esumpcvgval  31447  ofcfval4  31474  omssubadd  31668  carsggect  31686  plymulx0  31927  fdvneggt  31981  fdvnegge  31983  itgexpif  31987  ptpconn  32593  cvmliftlem6  32650  cvmliftlem8  32652  cvmlift2lem7  32669  cvmliftphtlem  32677  cvmlift3lem5  32683  elmsubrn  32888  knoppcnlem9  33953  curunc  35039  poimir  35090  broucube  35091  mblfinlem2  35095  volsupnfl  35102  cnambfre  35105  dvtan  35107  itg2addnclem  35108  itg2addnclem2  35109  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  itgaddnc  35117  itgmulc2nc  35125  ftc1cnnclem  35128  ftc1anclem1  35130  ftc1anclem2  35131  ftc1anclem3  35132  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  ftc2nc  35139  upixp  35167  fsuppssindlem1  39457  fsuppssindlem2  39458  mzpsubst  39689  diophun  39714  mendlmod  40137  mendassa  40138  fsovcnvlem  40714  binomcxplemnotnn0  41060  rnsnf  41810  cncfmptss  42229  climliminflimsupd  42443  mulcncff  42512  subcncff  42522  cncfcompt  42525  addcncff  42526  divcncff  42533  cncfiooicclem1  42535  dvsinexp  42553  dvsubf  42556  dvdivf  42564  dvcosax  42568  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  itgsinexplem1  42596  itgsubsticclem  42617  iblcncfioo  42620  itgiccshift  42622  stoweidlem20  42662  dirkercncflem2  42746  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem28  42777  fourierdlem39  42788  fourierdlem51  42799  fourierdlem60  42808  fourierdlem61  42809  fourierdlem69  42817  fourierdlem72  42820  fourierdlem73  42821  fourierdlem81  42829  fourierdlem83  42831  fourierdlem84  42832  fourierdlem87  42835  fourierdlem90  42838  fourierdlem93  42841  fourierdlem95  42843  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  etransclem34  42910  etransclem43  42919  etransclem46  42922  sge0tsms  43019  sge0fodjrnlem  43055  sge0iun  43058  sge0isum  43066  sge0seq  43085  meadjun  43101  meadjiunlem  43104  meadjiun  43105  ismeannd  43106  psmeasurelem  43109  omeiunle  43156  ovn02  43207  smfpimioo  43419  smfresal  43420  smfinflem  43448  smflimsuplem3  43453  smfliminflem  43461  1arymaptfo  45057  aacllem  45329  amgmwlem  45330  amgmlemALT  45331