Theorem feqmptd 6908

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

Syntax hints:   → wi 4   = wceq 1542   ↦ cmpt 5166   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  feqresmpt  6909  cofmpt  7085  fcoconst  7087  ofco  7656  caofinvl  7663  caofcom  7668  caofidlcan  7669  caofass  7671  caofdi  7673  caofdir  7674  caonncan  7675  suppssof1  8149  mapxpen  9081  xpmapenlem  9082  cantnfp1  9602  cantnflem1  9610  cnfcom2lem  9622  infxpenc  9940  pwfseqlem5  10586  gruf  10734  ccatco  14797  cnrecnv  15127  rlimclim1  15507  rlimuni  15512  lo1resb  15526  rlimresb  15527  o1resb  15528  rlimcn1  15550  rlimo1  15579  o1rlimmul  15581  caucvgr  15638  ackbijnn  15793  bitsf1ocnv  16413  ramcl  17000  pwsplusgval  17454  pwsmulrval  17455  pwsvscafval  17458  setcepi  18055  prf1st  18170  prf2nd  18171  1st2ndprf  18172  curfuncf  18204  curf2ndf  18213  yonedainv  18247  yonffthlem  18248  prdsidlem  18737  mhmvlin  18769  pwsco1mhm  18800  pwsco2mhm  18801  frmdup3lem  18834  frmdup3  18835  grpinvcnv  18982  pwsinvg  19029  pwssub  19030  efginvrel1  19703  frgpup3lem  19752  frgpup3  19753  gsumval3  19882  gsumcllem  19883  gsumzf1o  19887  gsumzsplit  19902  gsumconst  19909  gsumzmhm  19912  gsumsub  19923  gsum2dlem2  19946  gsumcom2  19950  dprdfadd  19997  dprdfsub  19998  dprdfeq0  19999  dprdf11  20000  dmdprdsplitlem  20014  dprddisj2  20016  dpjidcl  20035  ablfaclem2  20063  ablfac2  20066  rrgsupp  20678  mptscmfsuppd  20923  lmhmvsca  21040  mulgrhm2  21458  cygznlem2a  21547  frgpcyg  21553  uvcresum  21773  frlmup1  21778  gsumbagdiaglem  21910  psrass1lem  21912  psrlinv  21934  psrass1  21942  psrcom  21946  mplsubrglem  21982  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  evlslem2  22057  evlslem6  22059  evlslem1  22060  mhpmulcl  22115  psdmplcl  22128  psdmul  22132  coe1fval3  22172  coe1sclmul  22247  coe1sclmul2  22249  grpvrinv  22364  mdetleib2  22553  mdetunilem9  22585  cayleyhamilton1  22857  neiptopnei  23097  dfac14  23583  ptcnp  23587  lmcn2  23614  cnmpt11f  23629  cnmpt21f  23637  cnmpt2k  23653  qtopeu  23681  xkocnv  23779  xkohmeo  23780  flfcnp2  23972  istgp2  24056  tmdgsum  24060  subgtgp  24070  symgtgp  24071  tgpconncomp  24078  prdstgpd  24090  tsmssub  24114  tgptsmscls  24115  tsmssplit  24117  tsmsxplem1  24118  tlmtgp  24161  ustuqtop  24211  prdsmslem1  24492  prdsxmslem1  24493  prdsxmslem2  24494  tngnm  24616  nmoeq0  24701  cnfldnm  24743  cncfmpt1f  24881  negfcncf  24890  cnrehmeo  24920  evth  24926  evth2  24927  copco  24985  pcopt  24989  pcopt2  24990  pcoass  24991  pcorev2  24995  pi1xfrcnv  25024  ovolctb  25457  ovolfs2  25538  uniioombllem2  25550  ismbf  25595  mbfconst  25600  mbfmulc2re  25615  mbfadd  25628  mbfsub  25629  mbflimsup  25633  mbfi1flimlem  25689  mbfi1flim  25690  mbfmul  25693  itg2uba  25710  itg2mulclem  25713  itg2mulc  25714  itg2splitlem  25715  itg2monolem1  25717  itg2i1fseq  25722  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  i1fibl  25775  itgitg1  25776  bddmulibl  25806  bddiblnc  25809  cnplimc  25854  limccnp2  25859  dvcnp2  25887  dvmulf  25910  dvcmulf  25912  dvcobr  25913  dvcof  25915  dvcj  25917  dvfre  25918  dvmptcj  25935  dvcnvlem  25943  dvcnv  25944  dvef  25947  dvsincos  25948  rolle  25957  cmvth  25958  dvlip  25960  dvlipcn  25961  dv11cn  25968  dvivthlem1  25975  dvivth  25977  lhop2  25982  dvfsumrlim2  25999  ftc1lem1  26002  ftc1lem2  26003  ftc1a  26004  ftc1lem4  26006  ftc2  26011  ftc2ditglem  26012  ftc2ditg  26013  tdeglem4  26025  tdeglem2  26026  mdegle0  26042  mdegmullem  26043  plypf1  26177  plyco  26206  dgrcolem1  26238  dgrcolem2  26239  dgrco  26240  plycjlem  26241  dvply2g  26251  plydiveu  26264  elqaalem3  26287  taylthlem1  26338  taylthlem2  26339  ulmshft  26355  ulmdvlem1  26365  mtest  26369  mtestbdd  26370  mbfulm  26371  iblulm  26372  itgulm  26373  pserulm  26387  pserdv  26394  abelthlem1  26396  abelthlem3  26398  pige3ALT  26484  eff1olem  26512  logcn  26611  advlog  26618  advlogexp  26619  logtayl  26624  logccv  26627  dvcxp1  26704  dvcxp2  26705  dvcncxp1  26707  resqrtcn  26713  sqrtcn  26714  loglesqrt  26725  dvatan  26899  leibpi  26906  divsqrtsumo1  26947  jensenlem2  26951  amgmlem  26953  lgamgulmlem2  26993  ftalem7  27042  basellem9  27052  muinv  27156  dchrmullid  27215  dchrinvcl  27216  dchrisum0lem2a  27480  logdivsum  27496  mulog2sumlem1  27497  log2sumbnd  27507  hilnormi  31234  chscllem4  31711  hmopidmchi  32222  rabfodom  32575  ofoprabco  32737  fpwrelmapffslem  32805  fpwrelmap  32806  prodindf  32922  gsummulsubdishift1  33129  gsumwrd2dccat  33139  elrgspn  33307  elrgspnsubrunlem2  33309  domnprodeq0  33337  deg1prod  33643  mplmulmvr  33683  evlextv  33686  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmrhm  33691  psrgsum  33692  psrmonmul  33694  psrmonprod  33696  issply  33705  esplyfval0  33708  esplyfvaln  33718  lbsdiflsp0  33770  fedgmullem1  33773  extdgfialglem2  33837  qqhre  34164  esumpcvgval  34222  ofcfval4  34249  omssubadd  34444  carsggect  34462  plymulx0  34691  fdvneggt  34744  fdvnegge  34746  itgexpif  34750  ptpconn  35415  cvmliftlem6  35472  cvmliftlem8  35474  cvmlift2lem7  35491  cvmliftphtlem  35499  cvmlift3lem5  35505  elmsubrn  35710  knoppcnlem9  36761  curunc  37923  poimir  37974  broucube  37975  mblfinlem2  37979  volsupnfl  37986  cnambfre  37989  dvtan  37991  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  itgaddnc  38001  itgmulc2nc  38009  ftc1cnnclem  38012  ftc1anclem1  38014  ftc1anclem2  38015  ftc1anclem3  38016  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  upixp  38050  readvcot  42796  selvvvval  43018  evlselv  43020  fsuppssindlem1  43024  fsuppssindlem2  43025  mhphflem  43029  mhphf  43030  mzpsubst  43180  diophun  43205  mendlmod  43617  mendassa  43618  cantnf2  43753  fsovcnvlem  44440  binomcxplemnotnn0  44783  rnsnf  45614  cncfmptss  46017  climliminflimsupd  46229  mulcncff  46298  subcncff  46308  cncfcompt  46311  addcncff  46312  divcncff  46319  cncfiooicclem1  46321  dvsinexp  46339  dvsubf  46342  dvdivf  46350  dvcosax  46354  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  itgsinexplem1  46382  itgsubsticclem  46403  iblcncfioo  46406  itgiccshift  46408  stoweidlem20  46448  dirkercncflem2  46532  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem28  46563  fourierdlem39  46574  fourierdlem51  46585  fourierdlem60  46594  fourierdlem61  46595  fourierdlem69  46603  fourierdlem72  46606  fourierdlem73  46607  fourierdlem81  46615  fourierdlem83  46617  fourierdlem84  46618  fourierdlem87  46621  fourierdlem90  46624  fourierdlem93  46627  fourierdlem95  46629  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  etransclem34  46696  etransclem43  46705  etransclem46  46708  sge0tsms  46808  sge0fodjrnlem  46844  sge0iun  46847  sge0isum  46855  sge0seq  46874  meadjun  46890  meadjiunlem  46893  meadjiun  46894  ismeannd  46895  psmeasurelem  46898  omeiunle  46945  ovn02  46996  smfpimioo  47215  smfresal  47216  smfinflem  47245  smflimsuplem3  47250  smfliminflem  47258  1arymaptfo  49119  diag1  49779  aacllem  50276  amgmwlem  50277  amgmlemALT  50278