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 1542   ↦ cmpt 5167   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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  7079  fcoconst  7081  ofco  7649  caofinvl  7656  caofcom  7661  caofidlcan  7662  caofass  7664  caofdi  7666  caofdir  7667  caonncan  7668  suppssof1  8142  mapxpen  9074  xpmapenlem  9075  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  20669  mptscmfsuppd  20914  lmhmvsca  21032  mulgrhm2  21468  cygznlem2a  21557  frgpcyg  21563  uvcresum  21783  frlmup1  21788  gsumbagdiaglem  21920  psrass1lem  21922  psrlinv  21944  psrass1  21952  psrcom  21956  mplsubrglem  21992  mplmonmul  22024  mplcoe1  22025  mplcoe5  22028  evlslem2  22067  evlslem6  22069  evlslem1  22070  mhpmulcl  22125  psdmplcl  22138  psdmul  22142  coe1fval3  22182  coe1sclmul  22257  coe1sclmul2  22259  grpvrinv  22374  mdetleib2  22563  mdetunilem9  22595  cayleyhamilton1  22867  neiptopnei  23107  dfac14  23593  ptcnp  23597  lmcn2  23624  cnmpt11f  23639  cnmpt21f  23647  cnmpt2k  23663  qtopeu  23691  xkocnv  23789  xkohmeo  23790  flfcnp2  23982  istgp2  24066  tmdgsum  24070  subgtgp  24080  symgtgp  24081  tgpconncomp  24088  prdstgpd  24100  tsmssub  24124  tgptsmscls  24125  tsmssplit  24127  tsmsxplem1  24128  tlmtgp  24171  ustuqtop  24221  prdsmslem1  24502  prdsxmslem1  24503  prdsxmslem2  24504  tngnm  24626  nmoeq0  24711  cnfldnm  24753  cncfmpt1f  24891  negfcncf  24900  cnrehmeo  24930  evth  24936  evth2  24937  copco  24995  pcopt  24999  pcopt2  25000  pcoass  25001  pcorev2  25005  pi1xfrcnv  25034  ovolctb  25467  ovolfs2  25548  uniioombllem2  25560  ismbf  25605  mbfconst  25610  mbfmulc2re  25625  mbfadd  25638  mbfsub  25639  mbflimsup  25643  mbfi1flimlem  25699  mbfi1flim  25700  mbfmul  25703  itg2uba  25720  itg2mulclem  25723  itg2mulc  25724  itg2splitlem  25725  itg2monolem1  25727  itg2i1fseq  25732  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  i1fibl  25785  itgitg1  25786  bddmulibl  25816  bddiblnc  25819  cnplimc  25864  limccnp2  25869  dvcnp2  25897  dvmulf  25920  dvcmulf  25922  dvcobr  25923  dvcof  25925  dvcj  25927  dvfre  25928  dvmptcj  25945  dvcnvlem  25953  dvcnv  25954  dvef  25957  dvsincos  25958  rolle  25967  cmvth  25968  dvlip  25970  dvlipcn  25971  dv11cn  25978  dvivthlem1  25985  dvivth  25987  lhop2  25992  dvfsumrlim2  26009  ftc1lem1  26012  ftc1lem2  26013  ftc1a  26014  ftc1lem4  26016  ftc2  26021  ftc2ditglem  26022  ftc2ditg  26023  tdeglem4  26035  tdeglem2  26036  mdegle0  26052  mdegmullem  26053  plypf1  26187  plyco  26216  dgrcolem1  26248  dgrcolem2  26249  dgrco  26250  plycjlem  26251  dvply2g  26261  dvply2gOLD  26262  plydiveu  26275  elqaalem3  26298  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmshft  26368  ulmdvlem1  26378  mtest  26382  mtestbdd  26383  mbfulm  26384  iblulm  26385  itgulm  26386  pserulm  26400  pserdv  26407  abelthlem1  26409  abelthlem3  26411  pige3ALT  26497  eff1olem  26525  logcn  26624  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvcxp2  26718  dvcncxp1  26720  resqrtcn  26726  sqrtcn  26727  loglesqrt  26738  dvatan  26912  leibpi  26919  divsqrtsumo1  26961  jensenlem2  26965  amgmlem  26967  lgamgulmlem2  27007  ftalem7  27056  basellem9  27066  muinv  27170  dchrmullid  27229  dchrinvcl  27230  dchrisum0lem2a  27494  logdivsum  27510  mulog2sumlem1  27511  log2sumbnd  27521  hilnormi  31249  chscllem4  31726  hmopidmchi  32237  rabfodom  32590  ofoprabco  32752  fpwrelmapffslem  32820  fpwrelmap  32821  prodindf  32937  gsummulsubdishift1  33144  gsumwrd2dccat  33154  elrgspn  33322  elrgspnsubrunlem2  33324  domnprodeq0  33352  deg1prod  33658  mplmulmvr  33698  evlextv  33701  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmrhm  33706  psrgsum  33707  psrmonmul  33709  psrmonprod  33711  issply  33720  esplyfval0  33723  esplyfvaln  33733  lbsdiflsp0  33786  fedgmullem1  33789  extdgfialglem2  33853  qqhre  34180  esumpcvgval  34238  ofcfval4  34265  omssubadd  34460  carsggect  34478  plymulx0  34707  fdvneggt  34760  fdvnegge  34762  itgexpif  34766  ptpconn  35431  cvmliftlem6  35488  cvmliftlem8  35490  cvmlift2lem7  35507  cvmliftphtlem  35515  cvmlift3lem5  35521  elmsubrn  35726  knoppcnlem9  36777  curunc  37937  poimir  37988  broucube  37989  mblfinlem2  37993  volsupnfl  38000  cnambfre  38003  dvtan  38005  itg2addnclem  38006  itg2addnclem2  38007  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  itgaddnc  38015  itgmulc2nc  38023  ftc1cnnclem  38026  ftc1anclem1  38028  ftc1anclem2  38029  ftc1anclem3  38030  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  ftc2nc  38037  upixp  38064  readvcot  42810  selvvvval  43032  evlselv  43034  fsuppssindlem1  43038  fsuppssindlem2  43039  mhphflem  43043  mhphf  43044  mzpsubst  43194  diophun  43219  mendlmod  43635  mendassa  43636  cantnf2  43771  fsovcnvlem  44458  binomcxplemnotnn0  44801  rnsnf  45632  cncfmptss  46035  climliminflimsupd  46247  mulcncff  46316  subcncff  46326  cncfcompt  46329  addcncff  46330  divcncff  46337  cncfiooicclem1  46339  dvsinexp  46357  dvsubf  46360  dvdivf  46368  dvcosax  46372  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  itgsinexplem1  46400  itgsubsticclem  46421  iblcncfioo  46424  itgiccshift  46426  stoweidlem20  46466  dirkercncflem2  46550  fourierdlem16  46569  fourierdlem21  46574  fourierdlem22  46575  fourierdlem28  46581  fourierdlem39  46592  fourierdlem51  46603  fourierdlem60  46612  fourierdlem61  46613  fourierdlem69  46621  fourierdlem72  46624  fourierdlem73  46625  fourierdlem81  46633  fourierdlem83  46635  fourierdlem84  46636  fourierdlem87  46639  fourierdlem90  46642  fourierdlem93  46645  fourierdlem95  46647  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  etransclem34  46714  etransclem43  46723  etransclem46  46726  sge0tsms  46826  sge0fodjrnlem  46862  sge0iun  46865  sge0isum  46873  sge0seq  46892  meadjun  46908  meadjiunlem  46911  meadjiun  46912  ismeannd  46913  psmeasurelem  46916  omeiunle  46963  ovn02  47014  smfpimioo  47233  smfresal  47234  smfinflem  47263  smflimsuplem3  47268  smfliminflem  47276  1arymaptfo  49131  diag1  49791  aacllem  50288  amgmwlem  50289  amgmlemALT  50290