Theorem feqmptd 6834

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

Syntax hints:   → wi 4   = wceq 1542   ↦ cmpt 5162   Fn wfn 6427  ⟶wf 6428  ‘cfv 6432

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-fv 6440

This theorem is referenced by:  feqresmpt  6835  cofmpt  7001  fcoconst  7003  ofco  7550  caofinvl  7557  caofcom  7562  caofass  7564  caofdi  7566  caofdir  7567  caonncan  7568  suppssof1  8006  mapxpen  8912  xpmapenlem  8913  cantnfp1  9417  cantnflem1  9425  cnfcom2lem  9437  infxpenc  9775  pwfseqlem5  10420  gruf  10568  ccatco  14546  cnrecnv  14874  rlimclim1  15252  rlimuni  15257  lo1resb  15271  rlimresb  15272  o1resb  15273  rlimcn1  15295  rlimo1  15324  o1rlimmul  15326  caucvgr  15385  ackbijnn  15538  bitsf1ocnv  16149  ramcl  16728  pwsplusgval  17199  pwsmulrval  17200  pwsvscafval  17203  setcepi  17801  prf1st  17919  prf2nd  17920  1st2ndprf  17921  curfuncf  17954  curf2ndf  17963  yonedainv  17997  yonffthlem  17998  prdsidlem  18415  pwsco1mhm  18468  pwsco2mhm  18469  frmdup3lem  18503  frmdup3  18504  grpinvcnv  18641  pwsinvg  18686  pwssub  18687  efginvrel1  19332  frgpup3lem  19381  frgpup3  19382  gsumval3  19506  gsumcllem  19507  gsumzf1o  19511  gsumzsplit  19526  gsumconst  19533  gsumzmhm  19536  gsumsub  19547  gsum2dlem2  19570  gsumcom2  19574  dprdfadd  19621  dprdfsub  19622  dprdfeq0  19623  dprdf11  19624  dmdprdsplitlem  19638  dprddisj2  19640  dpjidcl  19659  ablfaclem2  19687  ablfac2  19690  mptscmfsuppd  20187  lmhmvsca  20305  rrgsupp  20560  mulgrhm2  20698  cygznlem2a  20773  frgpcyg  20779  uvcresum  20998  frlmup1  21003  psrbagaddclOLD  21130  gsumbagdiaglemOLD  21139  psrass1lemOLD  21141  gsumbagdiaglem  21142  psrass1lem  21144  psrlinv  21164  psrass1  21172  psrcom  21176  mplsubrglem  21208  mplmonmul  21235  mplcoe1  21236  mplcoe5  21239  evlslem2  21287  evlslem6  21289  evlslem1  21290  mhpmulcl  21337  coe1fval3  21377  coe1sclmul  21451  coe1sclmul2  21453  grpvrinv  21543  mhmvlin  21544  mdetleib2  21735  mdetunilem9  21767  cayleyhamilton1  22039  neiptopnei  22281  dfac14  22767  ptcnp  22771  lmcn2  22798  cnmpt11f  22813  cnmpt21f  22821  cnmpt2k  22837  qtopeu  22865  xkocnv  22963  xkohmeo  22964  flfcnp2  23156  istgp2  23240  tmdgsum  23244  subgtgp  23254  symgtgp  23255  tgpconncomp  23262  prdstgpd  23274  tsmssub  23298  tgptsmscls  23299  tsmssplit  23301  tsmsxplem1  23302  tlmtgp  23345  ustuqtop  23396  prdsmslem1  23681  prdsxmslem1  23682  prdsxmslem2  23683  tngnm  23813  nmoeq0  23898  cnfldnm  23940  cncfmpt1f  24075  negfcncf  24084  cnrehmeo  24114  evth  24120  evth2  24121  copco  24179  pcopt  24183  pcopt2  24184  pcoass  24185  pcorev2  24189  pi1xfrcnv  24218  ovolctb  24652  ovolfs2  24733  uniioombllem2  24745  ismbf  24790  mbfconst  24795  mbfmulc2re  24810  mbfadd  24823  mbfsub  24824  mbflimsup  24828  mbfi1flimlem  24885  mbfi1flim  24886  mbfmul  24889  itg2uba  24906  itg2mulclem  24909  itg2mulc  24910  itg2splitlem  24911  itg2monolem1  24913  itg2i1fseq  24918  itg2gt0  24923  itg2cnlem1  24924  itg2cnlem2  24925  i1fibl  24970  itgitg1  24971  bddmulibl  25001  bddiblnc  25004  cnplimc  25049  limccnp2  25054  dvcnp2  25082  dvmulf  25105  dvcmulf  25107  dvcobr  25108  dvcof  25110  dvcj  25112  dvfre  25113  dvmptcj  25130  dvcnvlem  25138  dvcnv  25139  dvef  25142  dvsincos  25143  rolle  25152  cmvth  25153  dvlip  25155  dvlipcn  25156  dv11cn  25163  dvivthlem1  25170  dvivth  25172  lhop2  25177  dvfsumrlim2  25194  ftc1lem1  25197  ftc1lem2  25198  ftc1a  25199  ftc1lem4  25201  ftc2  25206  ftc2ditglem  25207  ftc2ditg  25208  tdeglem4  25222  tdeglem4OLD  25223  tdeglem2  25224  mdegle0  25240  mdegmullem  25241  plypf1  25371  plyco  25400  dgrcolem1  25432  dgrcolem2  25433  dgrco  25434  plycjlem  25435  dvply2g  25443  plydiveu  25456  elqaalem3  25479  taylthlem1  25530  taylthlem2  25531  ulmshft  25547  ulmdvlem1  25557  mtest  25561  mtestbdd  25562  mbfulm  25563  iblulm  25564  itgulm  25565  pserulm  25579  pserdv  25586  abelthlem1  25588  abelthlem3  25590  pige3ALT  25674  eff1olem  25702  logcn  25800  advlog  25807  advlogexp  25808  logtayl  25813  logccv  25816  dvcxp1  25891  dvcxp2  25892  dvcncxp1  25894  resqrtcn  25900  sqrtcn  25901  loglesqrt  25909  dvatan  26083  leibpi  26090  divsqrtsumo1  26131  jensenlem2  26135  amgmlem  26137  lgamgulmlem2  26177  ftalem7  26226  basellem9  26236  muinv  26340  dchrmulid2  26398  dchrinvcl  26399  dchrisum0lem2a  26663  logdivsum  26679  mulog2sumlem1  26680  log2sumbnd  26690  hilnormi  29521  chscllem4  29998  hmopidmchi  30509  rabfodom  30847  ofoprabco  30997  fpwrelmapffslem  31063  fpwrelmap  31064  lbsdiflsp0  31703  fedgmullem1  31706  qqhre  31966  prodindf  31987  esumpcvgval  32042  ofcfval4  32069  omssubadd  32263  carsggect  32281  plymulx0  32522  fdvneggt  32576  fdvnegge  32578  itgexpif  32582  ptpconn  33191  cvmliftlem6  33248  cvmliftlem8  33250  cvmlift2lem7  33267  cvmliftphtlem  33275  cvmlift3lem5  33281  elmsubrn  33486  knoppcnlem9  34677  curunc  35755  poimir  35806  broucube  35807  mblfinlem2  35811  volsupnfl  35818  cnambfre  35821  dvtan  35823  itg2addnclem  35824  itg2addnclem2  35825  itg2addnclem3  35826  itg2addnc  35827  itg2gt0cn  35828  itgaddnc  35833  itgmulc2nc  35841  ftc1cnnclem  35844  ftc1anclem1  35846  ftc1anclem2  35847  ftc1anclem3  35848  ftc1anclem4  35849  ftc1anclem5  35850  ftc1anclem6  35851  ftc1anclem7  35852  ftc1anclem8  35853  ftc1anc  35854  ftc2nc  35855  upixp  35883  fsuppssindlem1  40277  fsuppssindlem2  40278  mhphflem  40281  mhphf  40282  mzpsubst  40567  diophun  40592  mendlmod  41015  mendassa  41016  fsovcnvlem  41591  binomcxplemnotnn0  41944  rnsnf  42691  cncfmptss  43099  climliminflimsupd  43313  mulcncff  43382  subcncff  43392  cncfcompt  43395  addcncff  43396  divcncff  43403  cncfiooicclem1  43405  dvsinexp  43423  dvsubf  43426  dvdivf  43434  dvcosax  43438  dvnmul  43455  dvnprodlem1  43458  dvnprodlem2  43459  itgsinexplem1  43466  itgsubsticclem  43487  iblcncfioo  43490  itgiccshift  43492  stoweidlem20  43532  dirkercncflem2  43616  fourierdlem16  43635  fourierdlem21  43640  fourierdlem22  43641  fourierdlem28  43647  fourierdlem39  43658  fourierdlem51  43669  fourierdlem60  43678  fourierdlem61  43679  fourierdlem69  43687  fourierdlem72  43690  fourierdlem73  43691  fourierdlem81  43699  fourierdlem83  43701  fourierdlem84  43702  fourierdlem87  43705  fourierdlem90  43708  fourierdlem93  43711  fourierdlem95  43713  fourierdlem101  43719  fourierdlem103  43721  fourierdlem104  43722  fourierdlem111  43729  etransclem34  43780  etransclem43  43789  etransclem46  43792  sge0tsms  43889  sge0fodjrnlem  43925  sge0iun  43928  sge0isum  43936  sge0seq  43955  meadjun  43971  meadjiunlem  43974  meadjiun  43975  ismeannd  43976  psmeasurelem  43979  omeiunle  44026  ovn02  44077  smfpimioo  44289  smfresal  44290  smfinflem  44318  smflimsuplem3  44323  smfliminflem  44331  1arymaptfo  45958  aacllem  46474  amgmwlem  46475  amgmlemALT  46476