Theorem funfnd 6580

Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
funfnd.1	⊢ (𝜑 → Fun 𝐴)

Assertion

Ref	Expression
funfnd	⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Proof of Theorem funfnd

Step	Hyp	Ref	Expression
1		funfnd.1	. 2 ⊢ (𝜑 → Fun 𝐴)
2		funfn 6579	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 217	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 5677  Fun wfun 6538   Fn wfn 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547

This theorem is referenced by:  fncofn  6667  resfunexg  7217  funiunfv  7247  funelss  8033  funsssuppss  8175  frrlem4  8274  wfrlem4OLD  8312  smores2  8354  tfrlem1  8376  resfnfinfin  9332  resfifsupp  9392  ordtypelem4  9516  ordtypelem9  9521  ordtypelem10  9522  brdom3  10523  brdom5  10524  brdom4  10525  fpwwe2lem10  10635  hashimarn  14400  resunimafz0  14404  isstruct2  17082  invf  17715  lindfrn  21376  ofco2  21953  dfac14  23122  perfdvf  25420  c1lip2  25515  taylf  25873  elno2  27157  noinfbnd2lem1  27233  noetainflem4  27243  lpvtx  28328  upgrle2  28365  uhgrvtxedgiedgb  28396  uhgr2edg  28465  ushgredgedg  28486  ushgredgedgloop  28488  subgruhgredgd  28541  subuhgr  28543  subupgr  28544  subumgr  28545  subusgr  28546  upgrres  28563  umgrres  28564  vtxdun  28738  upgrewlkle2  28863  eupthvdres  29488  cycpmfvlem  32271  cycpmfv3  32274  sitgf  33346  cardpred  34093  nummin  34094  bj-gabima  35820  gneispace  42885  gneispacef2  42887  funimaeq  43950  limsupresxr  44482  liminfresxr  44483  funcoressn  45752