Theorem feqmptd 6869

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

Syntax hints:   → wi 4   = wceq 1539   ↦ cmpt 5164   Fn wfn 6453  ⟶wf 6454  ‘cfv 6458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-fv 6466

This theorem is referenced by:  feqresmpt  6870  cofmpt  7036  fcoconst  7038  ofco  7588  caofinvl  7595  caofcom  7600  caofass  7602  caofdi  7604  caofdir  7605  caonncan  7606  suppssof1  8046  mapxpen  8968  xpmapenlem  8969  cantnfp1  9483  cantnflem1  9491  cnfcom2lem  9503  infxpenc  9820  pwfseqlem5  10465  gruf  10613  ccatco  14593  cnrecnv  14921  rlimclim1  15299  rlimuni  15304  lo1resb  15318  rlimresb  15319  o1resb  15320  rlimcn1  15342  rlimo1  15371  o1rlimmul  15373  caucvgr  15432  ackbijnn  15585  bitsf1ocnv  16196  ramcl  16775  pwsplusgval  17246  pwsmulrval  17247  pwsvscafval  17250  setcepi  17848  prf1st  17966  prf2nd  17967  1st2ndprf  17968  curfuncf  18001  curf2ndf  18010  yonedainv  18044  yonffthlem  18045  prdsidlem  18462  pwsco1mhm  18515  pwsco2mhm  18516  frmdup3lem  18550  frmdup3  18551  grpinvcnv  18688  pwsinvg  18733  pwssub  18734  efginvrel1  19379  frgpup3lem  19428  frgpup3  19429  gsumval3  19553  gsumcllem  19554  gsumzf1o  19558  gsumzsplit  19573  gsumconst  19580  gsumzmhm  19583  gsumsub  19594  gsum2dlem2  19617  gsumcom2  19621  dprdfadd  19668  dprdfsub  19669  dprdfeq0  19670  dprdf11  19671  dmdprdsplitlem  19685  dprddisj2  19687  dpjidcl  19706  ablfaclem2  19734  ablfac2  19737  mptscmfsuppd  20234  lmhmvsca  20352  rrgsupp  20607  mulgrhm2  20745  cygznlem2a  20820  frgpcyg  20826  uvcresum  21045  frlmup1  21050  psrbagaddclOLD  21177  gsumbagdiaglemOLD  21186  psrass1lemOLD  21188  gsumbagdiaglem  21189  psrass1lem  21191  psrlinv  21211  psrass1  21219  psrcom  21223  mplsubrglem  21255  mplmonmul  21282  mplcoe1  21283  mplcoe5  21286  evlslem2  21334  evlslem6  21336  evlslem1  21337  mhpmulcl  21384  coe1fval3  21424  coe1sclmul  21498  coe1sclmul2  21500  grpvrinv  21590  mhmvlin  21591  mdetleib2  21782  mdetunilem9  21814  cayleyhamilton1  22086  neiptopnei  22328  dfac14  22814  ptcnp  22818  lmcn2  22845  cnmpt11f  22860  cnmpt21f  22868  cnmpt2k  22884  qtopeu  22912  xkocnv  23010  xkohmeo  23011  flfcnp2  23203  istgp2  23287  tmdgsum  23291  subgtgp  23301  symgtgp  23302  tgpconncomp  23309  prdstgpd  23321  tsmssub  23345  tgptsmscls  23346  tsmssplit  23348  tsmsxplem1  23349  tlmtgp  23392  ustuqtop  23443  prdsmslem1  23728  prdsxmslem1  23729  prdsxmslem2  23730  tngnm  23860  nmoeq0  23945  cnfldnm  23987  cncfmpt1f  24122  negfcncf  24131  cnrehmeo  24161  evth  24167  evth2  24168  copco  24226  pcopt  24230  pcopt2  24231  pcoass  24232  pcorev2  24236  pi1xfrcnv  24265  ovolctb  24699  ovolfs2  24780  uniioombllem2  24792  ismbf  24837  mbfconst  24842  mbfmulc2re  24857  mbfadd  24870  mbfsub  24871  mbflimsup  24875  mbfi1flimlem  24932  mbfi1flim  24933  mbfmul  24936  itg2uba  24953  itg2mulclem  24956  itg2mulc  24957  itg2splitlem  24958  itg2monolem1  24960  itg2i1fseq  24965  itg2gt0  24970  itg2cnlem1  24971  itg2cnlem2  24972  i1fibl  25017  itgitg1  25018  bddmulibl  25048  bddiblnc  25051  cnplimc  25096  limccnp2  25101  dvcnp2  25129  dvmulf  25152  dvcmulf  25154  dvcobr  25155  dvcof  25157  dvcj  25159  dvfre  25160  dvmptcj  25177  dvcnvlem  25185  dvcnv  25186  dvef  25189  dvsincos  25190  rolle  25199  cmvth  25200  dvlip  25202  dvlipcn  25203  dv11cn  25210  dvivthlem1  25217  dvivth  25219  lhop2  25224  dvfsumrlim2  25241  ftc1lem1  25244  ftc1lem2  25245  ftc1a  25246  ftc1lem4  25248  ftc2  25253  ftc2ditglem  25254  ftc2ditg  25255  tdeglem4  25269  tdeglem4OLD  25270  tdeglem2  25271  mdegle0  25287  mdegmullem  25288  plypf1  25418  plyco  25447  dgrcolem1  25479  dgrcolem2  25480  dgrco  25481  plycjlem  25482  dvply2g  25490  plydiveu  25503  elqaalem3  25526  taylthlem1  25577  taylthlem2  25578  ulmshft  25594  ulmdvlem1  25604  mtest  25608  mtestbdd  25609  mbfulm  25610  iblulm  25611  itgulm  25612  pserulm  25626  pserdv  25633  abelthlem1  25635  abelthlem3  25637  pige3ALT  25721  eff1olem  25749  logcn  25847  advlog  25854  advlogexp  25855  logtayl  25860  logccv  25863  dvcxp1  25938  dvcxp2  25939  dvcncxp1  25941  resqrtcn  25947  sqrtcn  25948  loglesqrt  25956  dvatan  26130  leibpi  26137  divsqrtsumo1  26178  jensenlem2  26182  amgmlem  26184  lgamgulmlem2  26224  ftalem7  26273  basellem9  26283  muinv  26387  dchrmulid2  26445  dchrinvcl  26446  dchrisum0lem2a  26710  logdivsum  26726  mulog2sumlem1  26727  log2sumbnd  26737  hilnormi  29570  chscllem4  30047  hmopidmchi  30558  rabfodom  30896  ofoprabco  31046  fpwrelmapffslem  31112  fpwrelmap  31113  lbsdiflsp0  31752  fedgmullem1  31755  qqhre  32015  prodindf  32036  esumpcvgval  32091  ofcfval4  32118  omssubadd  32312  carsggect  32330  plymulx0  32571  fdvneggt  32625  fdvnegge  32627  itgexpif  32631  ptpconn  33240  cvmliftlem6  33297  cvmliftlem8  33299  cvmlift2lem7  33316  cvmliftphtlem  33324  cvmlift3lem5  33330  elmsubrn  33535  knoppcnlem9  34726  curunc  35803  poimir  35854  broucube  35855  mblfinlem2  35859  volsupnfl  35866  cnambfre  35869  dvtan  35871  itg2addnclem  35872  itg2addnclem2  35873  itg2addnclem3  35874  itg2addnc  35875  itg2gt0cn  35876  itgaddnc  35881  itgmulc2nc  35889  ftc1cnnclem  35892  ftc1anclem1  35894  ftc1anclem2  35895  ftc1anclem3  35896  ftc1anclem4  35897  ftc1anclem5  35898  ftc1anclem6  35899  ftc1anclem7  35900  ftc1anclem8  35901  ftc1anc  35902  ftc2nc  35903  upixp  35931  fsuppssindlem1  40317  fsuppssindlem2  40318  mhphflem  40321  mhphf  40322  mzpsubst  40607  diophun  40632  mendlmod  41056  mendassa  41057  fsovcnvlem  41659  binomcxplemnotnn0  42012  rnsnf  42765  cncfmptss  43177  climliminflimsupd  43391  mulcncff  43460  subcncff  43470  cncfcompt  43473  addcncff  43474  divcncff  43481  cncfiooicclem1  43483  dvsinexp  43501  dvsubf  43504  dvdivf  43512  dvcosax  43516  dvnmul  43533  dvnprodlem1  43536  dvnprodlem2  43537  itgsinexplem1  43544  itgsubsticclem  43565  iblcncfioo  43568  itgiccshift  43570  stoweidlem20  43610  dirkercncflem2  43694  fourierdlem16  43713  fourierdlem21  43718  fourierdlem22  43719  fourierdlem28  43725  fourierdlem39  43736  fourierdlem51  43747  fourierdlem60  43756  fourierdlem61  43757  fourierdlem69  43765  fourierdlem72  43768  fourierdlem73  43769  fourierdlem81  43777  fourierdlem83  43779  fourierdlem84  43780  fourierdlem87  43783  fourierdlem90  43786  fourierdlem93  43789  fourierdlem95  43791  fourierdlem101  43797  fourierdlem103  43799  fourierdlem104  43800  fourierdlem111  43807  etransclem34  43858  etransclem43  43867  etransclem46  43870  sge0tsms  43968  sge0fodjrnlem  44004  sge0iun  44007  sge0isum  44015  sge0seq  44034  meadjun  44050  meadjiunlem  44053  meadjiun  44054  ismeannd  44055  psmeasurelem  44058  omeiunle  44105  ovn02  44156  smfpimioo  44375  smfresal  44376  smfinflem  44404  smflimsuplem3  44409  smfliminflem  44417  1arymaptfo  46047  aacllem  46563  amgmwlem  46564  amgmlemALT  46565