Theorem feqmptd 6960

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5231   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is referenced by:  feqresmpt  6961  cofmpt  7132  fcoconst  7134  ofco  7696  caofinvl  7703  caofcom  7708  caofass  7710  caofdi  7712  caofdir  7713  caonncan  7714  suppssof1  8187  mapxpen  9146  xpmapenlem  9147  cantnfp1  9679  cantnflem1  9687  cnfcom2lem  9699  infxpenc  10016  pwfseqlem5  10661  gruf  10809  ccatco  14791  cnrecnv  15117  rlimclim1  15494  rlimuni  15499  lo1resb  15513  rlimresb  15514  o1resb  15515  rlimcn1  15537  rlimo1  15566  o1rlimmul  15568  caucvgr  15627  ackbijnn  15779  bitsf1ocnv  16390  ramcl  16967  pwsplusgval  17441  pwsmulrval  17442  pwsvscafval  17445  setcepi  18043  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18196  curf2ndf  18205  yonedainv  18239  yonffthlem  18240  prdsidlem  18692  pwsco1mhm  18750  pwsco2mhm  18751  frmdup3lem  18784  frmdup3  18785  grpinvcnv  18928  pwsinvg  18973  pwssub  18974  efginvrel1  19638  frgpup3lem  19687  frgpup3  19688  gsumval3  19817  gsumcllem  19818  gsumzf1o  19822  gsumzsplit  19837  gsumconst  19844  gsumzmhm  19847  gsumsub  19858  gsum2dlem2  19881  gsumcom2  19885  dprdfadd  19932  dprdfsub  19933  dprdfeq0  19934  dprdf11  19935  dmdprdsplitlem  19949  dprddisj2  19951  dpjidcl  19970  ablfaclem2  19998  ablfac2  20001  mptscmfsuppd  20683  lmhmvsca  20801  rrgsupp  21108  mulgrhm2  21250  cygznlem2a  21343  frgpcyg  21349  uvcresum  21568  frlmup1  21573  psrbagaddclOLD  21702  gsumbagdiaglemOLD  21711  psrass1lemOLD  21713  gsumbagdiaglem  21714  psrass1lem  21716  psrlinv  21736  psrass1  21745  psrcom  21749  mplsubrglem  21783  mplmonmul  21811  mplcoe1  21812  mplcoe5  21815  evlslem2  21862  evlslem6  21864  evlslem1  21865  mhpmulcl  21912  coe1fval3  21952  coe1sclmul  22025  coe1sclmul2  22027  grpvrinv  22119  mhmvlin  22120  mdetleib2  22311  mdetunilem9  22343  cayleyhamilton1  22615  neiptopnei  22857  dfac14  23343  ptcnp  23347  lmcn2  23374  cnmpt11f  23389  cnmpt21f  23397  cnmpt2k  23413  qtopeu  23441  xkocnv  23539  xkohmeo  23540  flfcnp2  23732  istgp2  23816  tmdgsum  23820  subgtgp  23830  symgtgp  23831  tgpconncomp  23838  prdstgpd  23850  tsmssub  23874  tgptsmscls  23875  tsmssplit  23877  tsmsxplem1  23878  tlmtgp  23921  ustuqtop  23972  prdsmslem1  24257  prdsxmslem1  24258  prdsxmslem2  24259  tngnm  24389  nmoeq0  24474  cnfldnm  24516  cncfmpt1f  24655  negfcncf  24665  cnrehmeo  24699  cnrehmeoOLD  24700  evth  24706  evth2  24707  copco  24766  pcopt  24770  pcopt2  24771  pcoass  24772  pcorev2  24776  pi1xfrcnv  24805  ovolctb  25240  ovolfs2  25321  uniioombllem2  25333  ismbf  25378  mbfconst  25383  mbfmulc2re  25398  mbfadd  25411  mbfsub  25412  mbflimsup  25416  mbfi1flimlem  25473  mbfi1flim  25474  mbfmul  25477  itg2uba  25494  itg2mulclem  25497  itg2mulc  25498  itg2splitlem  25499  itg2monolem1  25501  itg2i1fseq  25506  itg2gt0  25511  itg2cnlem1  25512  itg2cnlem2  25513  i1fibl  25558  itgitg1  25559  bddmulibl  25589  bddiblnc  25592  cnplimc  25637  limccnp2  25642  dvcnp2  25670  dvcnp2OLD  25671  dvmulf  25695  dvcmulf  25697  dvcobr  25698  dvcobrOLD  25699  dvcof  25701  dvcj  25703  dvfre  25704  dvmptcj  25721  dvcnvlem  25729  dvcnv  25730  dvef  25733  dvsincos  25734  rolle  25743  cmvth  25744  dvlip  25746  dvlipcn  25747  dv11cn  25754  dvivthlem1  25761  dvivth  25763  lhop2  25768  dvfsumrlim2  25785  ftc1lem1  25788  ftc1lem2  25789  ftc1a  25790  ftc1lem4  25792  ftc2  25797  ftc2ditglem  25798  ftc2ditg  25799  tdeglem4  25813  tdeglem4OLD  25814  tdeglem2  25815  mdegle0  25831  mdegmullem  25832  plypf1  25962  plyco  25991  dgrcolem1  26024  dgrcolem2  26025  dgrco  26026  plycjlem  26027  dvply2g  26035  plydiveu  26048  elqaalem3  26071  taylthlem1  26122  taylthlem2  26123  ulmshft  26139  ulmdvlem1  26149  mtest  26153  mtestbdd  26154  mbfulm  26155  iblulm  26156  itgulm  26157  pserulm  26171  pserdv  26178  abelthlem1  26180  abelthlem3  26182  pige3ALT  26266  eff1olem  26294  logcn  26392  advlog  26399  advlogexp  26400  logtayl  26405  logccv  26408  dvcxp1  26485  dvcxp2  26486  dvcncxp1  26488  resqrtcn  26494  sqrtcn  26495  loglesqrt  26503  dvatan  26677  leibpi  26684  divsqrtsumo1  26725  jensenlem2  26729  amgmlem  26731  lgamgulmlem2  26771  ftalem7  26820  basellem9  26830  muinv  26934  dchrmullid  26992  dchrinvcl  26993  dchrisum0lem2a  27257  logdivsum  27273  mulog2sumlem1  27274  log2sumbnd  27284  hilnormi  30684  chscllem4  31161  hmopidmchi  31672  rabfodom  32011  ofoprabco  32157  fpwrelmapffslem  32225  fpwrelmap  32226  lbsdiflsp0  33000  fedgmullem1  33003  qqhre  33299  prodindf  33320  esumpcvgval  33375  ofcfval4  33402  omssubadd  33598  carsggect  33616  plymulx0  33857  fdvneggt  33911  fdvnegge  33913  itgexpif  33917  ptpconn  34523  cvmliftlem6  34580  cvmliftlem8  34582  cvmlift2lem7  34599  cvmliftphtlem  34607  cvmlift3lem5  34613  elmsubrn  34818  gg-cmvth  35467  knoppcnlem9  35681  curunc  36774  poimir  36825  broucube  36826  mblfinlem2  36830  volsupnfl  36837  cnambfre  36840  dvtan  36842  itg2addnclem  36843  itg2addnclem2  36844  itg2addnclem3  36845  itg2addnc  36846  itg2gt0cn  36847  itgaddnc  36852  itgmulc2nc  36860  ftc1cnnclem  36863  ftc1anclem1  36865  ftc1anclem2  36866  ftc1anclem3  36867  ftc1anclem4  36868  ftc1anclem5  36869  ftc1anclem6  36870  ftc1anclem7  36871  ftc1anclem8  36872  ftc1anc  36873  ftc2nc  36874  upixp  36901  selvvvval  41460  evlselv  41462  fsuppssindlem1  41466  fsuppssindlem2  41467  mhphflem  41471  mhphf  41472  mzpsubst  41789  diophun  41814  mendlmod  42238  mendassa  42239  cantnf2  42378  fsovcnvlem  43067  binomcxplemnotnn0  43418  rnsnf  44182  cncfmptss  44602  climliminflimsupd  44816  mulcncff  44885  subcncff  44895  cncfcompt  44898  addcncff  44899  divcncff  44906  cncfiooicclem1  44908  dvsinexp  44926  dvsubf  44929  dvdivf  44937  dvcosax  44941  dvnmul  44958  dvnprodlem1  44961  dvnprodlem2  44962  itgsinexplem1  44969  itgsubsticclem  44990  iblcncfioo  44993  itgiccshift  44995  stoweidlem20  45035  dirkercncflem2  45119  fourierdlem16  45138  fourierdlem21  45143  fourierdlem22  45144  fourierdlem28  45150  fourierdlem39  45161  fourierdlem51  45172  fourierdlem60  45181  fourierdlem61  45182  fourierdlem69  45190  fourierdlem72  45193  fourierdlem73  45194  fourierdlem81  45202  fourierdlem83  45204  fourierdlem84  45205  fourierdlem87  45208  fourierdlem90  45211  fourierdlem93  45214  fourierdlem95  45216  fourierdlem101  45222  fourierdlem103  45224  fourierdlem104  45225  fourierdlem111  45232  etransclem34  45283  etransclem43  45292  etransclem46  45295  sge0tsms  45395  sge0fodjrnlem  45431  sge0iun  45434  sge0isum  45442  sge0seq  45461  meadjun  45477  meadjiunlem  45480  meadjiun  45481  ismeannd  45482  psmeasurelem  45485  omeiunle  45532  ovn02  45583  smfpimioo  45802  smfresal  45803  smfinflem  45832  smflimsuplem3  45837  smfliminflem  45845  1arymaptfo  47417  aacllem  47936  amgmwlem  47937  amgmlemALT  47938