Theorem feqmptd 6895

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

Syntax hints:   → wi 4   = wceq 1547   ↦ cmpt 5153   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493

This theorem is referenced by:  feqresmpt  6896  cofmpt  7074  fcoconst  7076  ofco  7645  caofinvl  7652  caofcom  7657  caofidlcan  7658  caofass  7660  caofdi  7662  caofdir  7663  caonncan  7664  suppssof1  8139  mapxpen  9071  xpmapenlem  9072  cantnfp1  9593  cantnflem1  9601  cnfcom2lem  9613  infxpenc  9931  pwfseqlem5  10577  gruf  10725  ccatco  14788  cnrecnv  15118  rlimclim1  15498  rlimuni  15503  lo1resb  15517  rlimresb  15518  o1resb  15519  rlimcn1  15541  rlimo1  15570  o1rlimmul  15572  caucvgr  15629  ackbijnn  15784  bitsf1ocnv  16404  ramcl  16991  pwsplusgval  17445  pwsmulrval  17446  pwsvscafval  17449  setcepi  18046  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18195  curf2ndf  18204  yonedainv  18238  yonffthlem  18239  prdsidlem  18728  mhmvlin  18760  pwsco1mhm  18791  pwsco2mhm  18792  frmdup3lem  18825  frmdup3  18826  grpinvcnv  18973  pwsinvg  19020  pwssub  19021  efginvrel1  19694  frgpup3lem  19743  frgpup3  19744  gsumval3  19873  gsumcllem  19874  gsumzf1o  19878  gsumzsplit  19893  gsumconst  19900  gsumzmhm  19903  gsumsub  19914  gsum2dlem2  19937  gsumcom2  19941  dprdfadd  19988  dprdfsub  19989  dprdfeq0  19990  dprdf11  19991  dmdprdsplitlem  20005  dprddisj2  20007  dpjidcl  20026  ablfaclem2  20054  ablfac2  20057  rrgsupp  20673  mptscmfsuppd  20918  lmhmvsca  21035  mulgrhm2  21453  cygznlem2a  21542  frgpcyg  21548  uvcresum  21768  frlmup1  21773  gsumbagdiaglem  21906  psrass1lem  21908  psrlinv  21930  psrass1  21938  psrcom  21942  mplsubrglem  21978  mplmonmul  22012  mplcoe1  22013  mplcoe5  22016  evlslem2  22055  evlslem6  22057  evlslem1  22058  selvvvval  22118  mhpmulcl  22137  psdmplcl  22150  psdmul  22154  coe1fval3  22193  coe1sclmul  22268  coe1sclmul2  22270  grpvrinv  22382  mdetleib2  22571  mdetunilem9  22603  cayleyhamilton1  22875  neiptopnei  23115  dfac14  23601  ptcnp  23605  lmcn2  23632  cnmpt11f  23647  cnmpt21f  23655  cnmpt2k  23671  qtopeu  23699  xkocnv  23797  xkohmeo  23798  flfcnp2  23990  istgp2  24074  tmdgsum  24078  subgtgp  24088  symgtgp  24089  tgpconncomp  24096  prdstgpd  24108  tsmssub  24132  tgptsmscls  24133  tsmssplit  24135  tsmsxplem1  24136  tlmtgp  24179  ustuqtop  24229  prdsmslem1  24510  prdsxmslem1  24511  prdsxmslem2  24512  tngnm  24634  nmoeq0  24719  cnfldnm  24761  cncfmpt1f  24899  negfcncf  24908  cnrehmeo  24938  evth  24944  evth2  24945  copco  25003  pcopt  25007  pcopt2  25008  pcoass  25009  pcorev2  25013  pi1xfrcnv  25042  ovolctb  25475  ovolfs2  25556  uniioombllem2  25568  ismbf  25613  mbfconst  25618  mbfmulc2re  25633  mbfadd  25646  mbfsub  25647  mbflimsup  25651  mbfi1flimlem  25707  mbfi1flim  25708  mbfmul  25711  itg2uba  25728  itg2mulclem  25731  itg2mulc  25732  itg2splitlem  25733  itg2monolem1  25735  itg2i1fseq  25740  itg2gt0  25745  itg2cnlem1  25746  itg2cnlem2  25747  i1fibl  25793  itgitg1  25794  bddmulibl  25824  bddiblnc  25827  cnplimc  25872  limccnp2  25877  dvcnp2  25905  dvmulf  25928  dvcmulf  25930  dvcobr  25931  dvcof  25933  dvcj  25935  dvfre  25936  dvmptcj  25953  dvcnvlem  25961  dvcnv  25962  dvef  25965  dvsincos  25966  rolle  25975  cmvth  25976  dvlip  25978  dvlipcn  25979  dv11cn  25986  dvivthlem1  25993  dvivth  25995  lhop2  26000  dvfsumrlim2  26017  ftc1lem1  26020  ftc1lem2  26021  ftc1a  26022  ftc1lem4  26024  ftc2  26029  ftc2ditglem  26030  ftc2ditg  26031  tdeglem4  26043  tdeglem2  26044  mdegle0  26060  mdegmullem  26061  plypf1  26195  plyco  26224  dgrcolem1  26256  dgrcolem2  26257  dgrco  26258  plycjlem  26259  dvply2g  26269  plydiveu  26282  elqaalem3  26305  taylthlem1  26356  taylthlem2  26357  ulmshft  26373  ulmdvlem1  26383  mtest  26387  mtestbdd  26388  mbfulm  26389  iblulm  26390  itgulm  26391  pserulm  26405  pserdv  26412  abelthlem1  26414  abelthlem3  26416  pige3ALT  26502  eff1olem  26530  logcn  26629  advlog  26636  advlogexp  26637  logtayl  26642  logccv  26645  dvcxp1  26722  dvcxp2  26723  dvcncxp1  26725  resqrtcn  26731  sqrtcn  26732  loglesqrt  26743  dvatan  26917  leibpi  26924  divsqrtsumo1  26965  jensenlem2  26969  amgmlem  26971  lgamgulmlem2  27011  ftalem7  27060  basellem9  27070  muinv  27174  dchrmullid  27233  dchrinvcl  27234  dchrisum0lem2a  27498  logdivsum  27514  mulog2sumlem1  27515  log2sumbnd  27525  hilnormi  31252  chscllem4  31729  hmopidmchi  32240  rabfodom  32593  ofoprabco  32756  fpwrelmapffslem  32824  fpwrelmap  32825  prodindf  32941  gsummulsubdishift1  33149  gsumwrd2dccat  33159  elrgspn  33327  elrgspnsubrunlem2  33329  domnprodeq0  33357  deg1prod  33666  selvply1rhmlem2  33705  selvply1rhmlem4  33707  selvply1rhm0  33710  mplmulmvr  33723  evlextv  33726  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmrhm  33731  psrgsum  33732  psrmonmul  33734  psrmonprod  33736  issply  33745  esplyfval0  33748  esplyfvaln  33758  lbsdiflsp0  33810  fedgmullem1  33813  extdgfialglem2  33877  qqhre  34204  esumpcvgval  34262  ofcfval4  34289  omssubadd  34484  carsggect  34502  plymulx0  34731  fdvneggt  34784  fdvnegge  34786  itgexpif  34790  ptpconn  35461  cvmliftlem6  35518  cvmliftlem8  35520  cvmlift2lem7  35537  cvmliftphtlem  35545  cvmlift3lem5  35551  elmsubrn  35756  knoppcnlem9  36807  curunc  37969  poimir  38020  broucube  38021  mblfinlem2  38025  volsupnfl  38032  cnambfre  38035  dvtan  38037  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  itgaddnc  38047  itgmulc2nc  38055  ftc1cnnclem  38058  ftc1anclem1  38060  ftc1anclem2  38061  ftc1anclem3  38062  ftc1anclem4  38063  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  ftc2nc  38069  upixp  38096  readvcot  42841  evlselv  43039  fsuppssindlem1  43041  fsuppssindlem2  43042  mhphflem  43046  mhphf  43047  mzpsubst  43197  diophun  43222  mendlmod  43634  mendassa  43635  cantnf2  43770  fsovcnvlem  44457  binomcxplemnotnn0  44800  rnsnf  45631  cncfmptss  46032  climliminflimsupd  46244  mulcncff  46313  subcncff  46323  cncfcompt  46326  addcncff  46327  divcncff  46334  cncfiooicclem1  46336  dvsinexp  46354  dvsubf  46357  dvdivf  46365  dvcosax  46369  dvnmul  46386  dvnprodlem1  46389  dvnprodlem2  46390  itgsinexplem1  46397  itgsubsticclem  46418  iblcncfioo  46421  itgiccshift  46423  stoweidlem20  46463  dirkercncflem2  46547  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem28  46578  fourierdlem39  46589  fourierdlem51  46600  fourierdlem60  46609  fourierdlem61  46610  fourierdlem69  46618  fourierdlem72  46621  fourierdlem73  46622  fourierdlem81  46630  fourierdlem83  46632  fourierdlem84  46633  fourierdlem87  46636  fourierdlem90  46639  fourierdlem93  46642  fourierdlem95  46644  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  etransclem34  46711  etransclem43  46720  etransclem46  46723  sge0tsms  46823  sge0fodjrnlem  46859  sge0iun  46862  sge0isum  46870  sge0seq  46889  meadjun  46905  meadjiunlem  46908  meadjiun  46909  ismeannd  46910  psmeasurelem  46913  omeiunle  46960  ovn02  47011  smfpimioo  47230  smfresal  47231  smfinflem  47260  smflimsuplem3  47265  smfliminflem  47273  1arymaptfo  49134  diag1  49794  aacllem  50291  amgmwlem  50292  amgmlemALT  50293