Theorem feqmptd 6899

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5176   Fn wfn 6484  ⟶wf 6485  ‘cfv 6489

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497

This theorem is referenced by:  feqresmpt  6900  cofmpt  7074  fcoconst  7076  ofco  7644  caofinvl  7651  caofcom  7656  caofidlcan  7657  caofass  7659  caofdi  7661  caofdir  7662  caonncan  7663  suppssof1  8138  mapxpen  9067  xpmapenlem  9068  cantnfp1  9582  cantnflem1  9590  cnfcom2lem  9602  infxpenc  9920  pwfseqlem5  10565  gruf  10713  ccatco  14749  cnrecnv  15079  rlimclim1  15459  rlimuni  15464  lo1resb  15478  rlimresb  15479  o1resb  15480  rlimcn1  15502  rlimo1  15531  o1rlimmul  15533  caucvgr  15590  ackbijnn  15742  bitsf1ocnv  16362  ramcl  16948  pwsplusgval  17402  pwsmulrval  17403  pwsvscafval  17406  setcepi  18003  prf1st  18118  prf2nd  18119  1st2ndprf  18120  curfuncf  18152  curf2ndf  18161  yonedainv  18195  yonffthlem  18196  prdsidlem  18685  mhmvlin  18717  pwsco1mhm  18748  pwsco2mhm  18749  frmdup3lem  18782  frmdup3  18783  grpinvcnv  18927  pwsinvg  18974  pwssub  18975  efginvrel1  19648  frgpup3lem  19697  frgpup3  19698  gsumval3  19827  gsumcllem  19828  gsumzf1o  19832  gsumzsplit  19847  gsumconst  19854  gsumzmhm  19857  gsumsub  19868  gsum2dlem2  19891  gsumcom2  19895  dprdfadd  19942  dprdfsub  19943  dprdfeq0  19944  dprdf11  19945  dmdprdsplitlem  19959  dprddisj2  19961  dpjidcl  19980  ablfaclem2  20008  ablfac2  20011  rrgsupp  20625  mptscmfsuppd  20870  lmhmvsca  20988  mulgrhm2  21424  cygznlem2a  21513  frgpcyg  21519  uvcresum  21739  frlmup1  21744  gsumbagdiaglem  21877  psrass1lem  21879  psrlinv  21902  psrass1  21910  psrcom  21914  mplsubrglem  21950  mplmonmul  21982  mplcoe1  21983  mplcoe5  21986  evlslem2  22025  evlslem6  22027  evlslem1  22028  mhpmulcl  22083  psdmplcl  22096  psdmul  22100  coe1fval3  22140  coe1sclmul  22215  coe1sclmul2  22217  grpvrinv  22334  mdetleib2  22523  mdetunilem9  22555  cayleyhamilton1  22827  neiptopnei  23067  dfac14  23553  ptcnp  23557  lmcn2  23584  cnmpt11f  23599  cnmpt21f  23607  cnmpt2k  23623  qtopeu  23651  xkocnv  23749  xkohmeo  23750  flfcnp2  23942  istgp2  24026  tmdgsum  24030  subgtgp  24040  symgtgp  24041  tgpconncomp  24048  prdstgpd  24060  tsmssub  24084  tgptsmscls  24085  tsmssplit  24087  tsmsxplem1  24088  tlmtgp  24131  ustuqtop  24181  prdsmslem1  24462  prdsxmslem1  24463  prdsxmslem2  24464  tngnm  24586  nmoeq0  24671  cnfldnm  24713  cncfmpt1f  24854  negfcncf  24864  cnrehmeo  24898  cnrehmeoOLD  24899  evth  24905  evth2  24906  copco  24965  pcopt  24969  pcopt2  24970  pcoass  24971  pcorev2  24975  pi1xfrcnv  25004  ovolctb  25438  ovolfs2  25519  uniioombllem2  25531  ismbf  25576  mbfconst  25581  mbfmulc2re  25596  mbfadd  25609  mbfsub  25610  mbflimsup  25614  mbfi1flimlem  25670  mbfi1flim  25671  mbfmul  25674  itg2uba  25691  itg2mulclem  25694  itg2mulc  25695  itg2splitlem  25696  itg2monolem1  25698  itg2i1fseq  25703  itg2gt0  25708  itg2cnlem1  25709  itg2cnlem2  25710  i1fibl  25756  itgitg1  25757  bddmulibl  25787  bddiblnc  25790  cnplimc  25835  limccnp2  25840  dvcnp2  25868  dvcnp2OLD  25869  dvmulf  25893  dvcmulf  25895  dvcobr  25896  dvcobrOLD  25897  dvcof  25899  dvcj  25901  dvfre  25902  dvmptcj  25919  dvcnvlem  25927  dvcnv  25928  dvef  25931  dvsincos  25932  rolle  25941  cmvth  25942  cmvthOLD  25943  dvlip  25945  dvlipcn  25946  dv11cn  25953  dvivthlem1  25960  dvivth  25962  lhop2  25967  dvfsumrlim2  25986  ftc1lem1  25989  ftc1lem2  25990  ftc1a  25991  ftc1lem4  25993  ftc2  25998  ftc2ditglem  25999  ftc2ditg  26000  tdeglem4  26012  tdeglem2  26013  mdegle0  26029  mdegmullem  26030  plypf1  26164  plyco  26193  dgrcolem1  26226  dgrcolem2  26227  dgrco  26228  plycjlem  26229  dvply2g  26239  dvply2gOLD  26240  plydiveu  26253  elqaalem3  26276  taylthlem1  26328  taylthlem2  26329  taylthlem2OLD  26330  ulmshft  26346  ulmdvlem1  26356  mtest  26360  mtestbdd  26361  mbfulm  26362  iblulm  26363  itgulm  26364  pserulm  26378  pserdv  26386  abelthlem1  26388  abelthlem3  26390  pige3ALT  26476  eff1olem  26504  logcn  26603  advlog  26610  advlogexp  26611  logtayl  26616  logccv  26619  dvcxp1  26696  dvcxp2  26697  dvcncxp1  26699  resqrtcn  26706  sqrtcn  26707  loglesqrt  26718  dvatan  26892  leibpi  26899  divsqrtsumo1  26941  jensenlem2  26945  amgmlem  26947  lgamgulmlem2  26987  ftalem7  27036  basellem9  27046  muinv  27150  dchrmullid  27210  dchrinvcl  27211  dchrisum0lem2a  27475  logdivsum  27491  mulog2sumlem1  27492  log2sumbnd  27502  hilnormi  31164  chscllem4  31641  hmopidmchi  32152  rabfodom  32506  ofoprabco  32668  fpwrelmapffslem  32739  fpwrelmap  32740  prodindf  32872  gsummulsubdishift1  33079  gsumwrd2dccat  33088  elrgspn  33256  elrgspnsubrunlem2  33258  domnprodeq0  33286  deg1prod  33592  mplmulmvr  33632  evlextv  33635  mplvrpmfgalem  33637  mplvrpmga  33638  mplvrpmrhm  33640  issply  33647  esplyfval0  33650  lbsdiflsp0  33711  fedgmullem1  33714  extdgfialglem2  33778  qqhre  34105  esumpcvgval  34163  ofcfval4  34190  omssubadd  34385  carsggect  34403  plymulx0  34632  fdvneggt  34685  fdvnegge  34687  itgexpif  34691  ptpconn  35349  cvmliftlem6  35406  cvmliftlem8  35408  cvmlift2lem7  35425  cvmliftphtlem  35433  cvmlift3lem5  35439  elmsubrn  35644  knoppcnlem9  36617  curunc  37715  poimir  37766  broucube  37767  mblfinlem2  37771  volsupnfl  37778  cnambfre  37781  dvtan  37783  itg2addnclem  37784  itg2addnclem2  37785  itg2addnclem3  37786  itg2addnc  37787  itg2gt0cn  37788  itgaddnc  37793  itgmulc2nc  37801  ftc1cnnclem  37804  ftc1anclem1  37806  ftc1anclem2  37807  ftc1anclem3  37808  ftc1anclem4  37809  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  ftc2nc  37815  upixp  37842  readvcot  42534  selvvvval  42743  evlselv  42745  fsuppssindlem1  42749  fsuppssindlem2  42750  mhphflem  42754  mhphf  42755  mzpsubst  42905  diophun  42930  mendlmod  43346  mendassa  43347  cantnf2  43482  fsovcnvlem  44170  binomcxplemnotnn0  44513  rnsnf  45344  cncfmptss  45749  climliminflimsupd  45961  mulcncff  46030  subcncff  46040  cncfcompt  46043  addcncff  46044  divcncff  46051  cncfiooicclem1  46053  dvsinexp  46071  dvsubf  46074  dvdivf  46082  dvcosax  46086  dvnmul  46103  dvnprodlem1  46106  dvnprodlem2  46107  itgsinexplem1  46114  itgsubsticclem  46135  iblcncfioo  46138  itgiccshift  46140  stoweidlem20  46180  dirkercncflem2  46264  fourierdlem16  46283  fourierdlem21  46288  fourierdlem22  46289  fourierdlem28  46295  fourierdlem39  46306  fourierdlem51  46317  fourierdlem60  46326  fourierdlem61  46327  fourierdlem69  46335  fourierdlem72  46338  fourierdlem73  46339  fourierdlem81  46347  fourierdlem83  46349  fourierdlem84  46350  fourierdlem87  46353  fourierdlem90  46356  fourierdlem93  46359  fourierdlem95  46361  fourierdlem101  46367  fourierdlem103  46369  fourierdlem104  46370  fourierdlem111  46377  etransclem34  46428  etransclem43  46437  etransclem46  46440  sge0tsms  46540  sge0fodjrnlem  46576  sge0iun  46579  sge0isum  46587  sge0seq  46606  meadjun  46622  meadjiunlem  46625  meadjiun  46626  ismeannd  46627  psmeasurelem  46630  omeiunle  46677  ovn02  46728  smfpimioo  46947  smfresal  46948  smfinflem  46977  smflimsuplem3  46982  smfliminflem  46990  1arymaptfo  48805  diag1  49465  aacllem  49962  amgmwlem  49963  amgmlemALT  49964