Theorem feqmptd 6959

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

Syntax hints:   → wi 4   = wceq 1539   ↦ cmpt 5230   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542

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 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  feqresmpt  6960  cofmpt  7131  fcoconst  7133  ofco  7695  caofinvl  7702  caofcom  7707  caofass  7709  caofdi  7711  caofdir  7712  caonncan  7713  suppssof1  8186  mapxpen  9145  xpmapenlem  9146  cantnfp1  9678  cantnflem1  9686  cnfcom2lem  9698  infxpenc  10015  pwfseqlem5  10660  gruf  10808  ccatco  14790  cnrecnv  15116  rlimclim1  15493  rlimuni  15498  lo1resb  15512  rlimresb  15513  o1resb  15514  rlimcn1  15536  rlimo1  15565  o1rlimmul  15567  caucvgr  15626  ackbijnn  15778  bitsf1ocnv  16389  ramcl  16966  pwsplusgval  17440  pwsmulrval  17441  pwsvscafval  17444  setcepi  18042  prf1st  18160  prf2nd  18161  1st2ndprf  18162  curfuncf  18195  curf2ndf  18204  yonedainv  18238  yonffthlem  18239  prdsidlem  18691  pwsco1mhm  18749  pwsco2mhm  18750  frmdup3lem  18783  frmdup3  18784  grpinvcnv  18927  pwsinvg  18972  pwssub  18973  efginvrel1  19637  frgpup3lem  19686  frgpup3  19687  gsumval3  19816  gsumcllem  19817  gsumzf1o  19821  gsumzsplit  19836  gsumconst  19843  gsumzmhm  19846  gsumsub  19857  gsum2dlem2  19880  gsumcom2  19884  dprdfadd  19931  dprdfsub  19932  dprdfeq0  19933  dprdf11  19934  dmdprdsplitlem  19948  dprddisj2  19950  dpjidcl  19969  ablfaclem2  19997  ablfac2  20000  mptscmfsuppd  20682  lmhmvsca  20800  rrgsupp  21107  mulgrhm2  21249  cygznlem2a  21342  frgpcyg  21348  uvcresum  21567  frlmup1  21572  psrbagaddclOLD  21701  gsumbagdiaglemOLD  21710  psrass1lemOLD  21712  gsumbagdiaglem  21713  psrass1lem  21715  psrlinv  21735  psrass1  21744  psrcom  21748  mplsubrglem  21782  mplmonmul  21810  mplcoe1  21811  mplcoe5  21814  evlslem2  21861  evlslem6  21863  evlslem1  21864  mhpmulcl  21911  coe1fval3  21951  coe1sclmul  22024  coe1sclmul2  22026  grpvrinv  22118  mhmvlin  22119  mdetleib2  22310  mdetunilem9  22342  cayleyhamilton1  22614  neiptopnei  22856  dfac14  23342  ptcnp  23346  lmcn2  23373  cnmpt11f  23388  cnmpt21f  23396  cnmpt2k  23412  qtopeu  23440  xkocnv  23538  xkohmeo  23539  flfcnp2  23731  istgp2  23815  tmdgsum  23819  subgtgp  23829  symgtgp  23830  tgpconncomp  23837  prdstgpd  23849  tsmssub  23873  tgptsmscls  23874  tsmssplit  23876  tsmsxplem1  23877  tlmtgp  23920  ustuqtop  23971  prdsmslem1  24256  prdsxmslem1  24257  prdsxmslem2  24258  tngnm  24388  nmoeq0  24473  cnfldnm  24515  cncfmpt1f  24654  negfcncf  24664  cnrehmeo  24698  cnrehmeoOLD  24699  evth  24705  evth2  24706  copco  24765  pcopt  24769  pcopt2  24770  pcoass  24771  pcorev2  24775  pi1xfrcnv  24804  ovolctb  25239  ovolfs2  25320  uniioombllem2  25332  ismbf  25377  mbfconst  25382  mbfmulc2re  25397  mbfadd  25410  mbfsub  25411  mbflimsup  25415  mbfi1flimlem  25472  mbfi1flim  25473  mbfmul  25476  itg2uba  25493  itg2mulclem  25496  itg2mulc  25497  itg2splitlem  25498  itg2monolem1  25500  itg2i1fseq  25505  itg2gt0  25510  itg2cnlem1  25511  itg2cnlem2  25512  i1fibl  25557  itgitg1  25558  bddmulibl  25588  bddiblnc  25591  cnplimc  25636  limccnp2  25641  dvcnp2  25669  dvcnp2OLD  25670  dvmulf  25694  dvcmulf  25696  dvcobr  25697  dvcobrOLD  25698  dvcof  25700  dvcj  25702  dvfre  25703  dvmptcj  25720  dvcnvlem  25728  dvcnv  25729  dvef  25732  dvsincos  25733  rolle  25742  cmvth  25743  dvlip  25745  dvlipcn  25746  dv11cn  25753  dvivthlem1  25760  dvivth  25762  lhop2  25767  dvfsumrlim2  25784  ftc1lem1  25787  ftc1lem2  25788  ftc1a  25789  ftc1lem4  25791  ftc2  25796  ftc2ditglem  25797  ftc2ditg  25798  tdeglem4  25812  tdeglem4OLD  25813  tdeglem2  25814  mdegle0  25830  mdegmullem  25831  plypf1  25961  plyco  25990  dgrcolem1  26023  dgrcolem2  26024  dgrco  26025  plycjlem  26026  dvply2g  26034  plydiveu  26047  elqaalem3  26070  taylthlem1  26121  taylthlem2  26122  ulmshft  26138  ulmdvlem1  26148  mtest  26152  mtestbdd  26153  mbfulm  26154  iblulm  26155  itgulm  26156  pserulm  26170  pserdv  26177  abelthlem1  26179  abelthlem3  26181  pige3ALT  26265  eff1olem  26293  logcn  26391  advlog  26398  advlogexp  26399  logtayl  26404  logccv  26407  dvcxp1  26484  dvcxp2  26485  dvcncxp1  26487  resqrtcn  26493  sqrtcn  26494  loglesqrt  26502  dvatan  26676  leibpi  26683  divsqrtsumo1  26724  jensenlem2  26728  amgmlem  26730  lgamgulmlem2  26770  ftalem7  26819  basellem9  26829  muinv  26933  dchrmullid  26991  dchrinvcl  26992  dchrisum0lem2a  27256  logdivsum  27272  mulog2sumlem1  27273  log2sumbnd  27283  hilnormi  30683  chscllem4  31160  hmopidmchi  31671  rabfodom  32010  ofoprabco  32156  fpwrelmapffslem  32224  fpwrelmap  32225  lbsdiflsp0  32999  fedgmullem1  33002  qqhre  33298  prodindf  33319  esumpcvgval  33374  ofcfval4  33401  omssubadd  33597  carsggect  33615  plymulx0  33856  fdvneggt  33910  fdvnegge  33912  itgexpif  33916  ptpconn  34522  cvmliftlem6  34579  cvmliftlem8  34581  cvmlift2lem7  34598  cvmliftphtlem  34606  cvmlift3lem5  34612  elmsubrn  34817  gg-cmvth  35466  knoppcnlem9  35680  curunc  36773  poimir  36824  broucube  36825  mblfinlem2  36829  volsupnfl  36836  cnambfre  36839  dvtan  36841  itg2addnclem  36842  itg2addnclem2  36843  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  itgaddnc  36851  itgmulc2nc  36859  ftc1cnnclem  36862  ftc1anclem1  36864  ftc1anclem2  36865  ftc1anclem3  36866  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  ftc2nc  36873  upixp  36900  selvvvval  41459  evlselv  41461  fsuppssindlem1  41465  fsuppssindlem2  41466  mhphflem  41470  mhphf  41471  mzpsubst  41788  diophun  41813  mendlmod  42237  mendassa  42238  cantnf2  42377  fsovcnvlem  43066  binomcxplemnotnn0  43417  rnsnf  44181  cncfmptss  44601  climliminflimsupd  44815  mulcncff  44884  subcncff  44894  cncfcompt  44897  addcncff  44898  divcncff  44905  cncfiooicclem1  44907  dvsinexp  44925  dvsubf  44928  dvdivf  44936  dvcosax  44940  dvnmul  44957  dvnprodlem1  44960  dvnprodlem2  44961  itgsinexplem1  44968  itgsubsticclem  44989  iblcncfioo  44992  itgiccshift  44994  stoweidlem20  45034  dirkercncflem2  45118  fourierdlem16  45137  fourierdlem21  45142  fourierdlem22  45143  fourierdlem28  45149  fourierdlem39  45160  fourierdlem51  45171  fourierdlem60  45180  fourierdlem61  45181  fourierdlem69  45189  fourierdlem72  45192  fourierdlem73  45193  fourierdlem81  45201  fourierdlem83  45203  fourierdlem84  45204  fourierdlem87  45207  fourierdlem90  45210  fourierdlem93  45213  fourierdlem95  45215  fourierdlem101  45221  fourierdlem103  45223  fourierdlem104  45224  fourierdlem111  45231  etransclem34  45282  etransclem43  45291  etransclem46  45294  sge0tsms  45394  sge0fodjrnlem  45430  sge0iun  45433  sge0isum  45441  sge0seq  45460  meadjun  45476  meadjiunlem  45479  meadjiun  45480  ismeannd  45481  psmeasurelem  45484  omeiunle  45531  ovn02  45582  smfpimioo  45801  smfresal  45802  smfinflem  45831  smflimsuplem3  45836  smfliminflem  45844  1arymaptfo  47416  aacllem  47935  amgmwlem  47936  amgmlemALT  47937