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  28359  upgrle2  28396  uhgrvtxedgiedgb  28427  uhgr2edg  28496  ushgredgedg  28517  ushgredgedgloop  28519  subgruhgredgd  28572  subuhgr  28574  subupgr  28575  subumgr  28576  subusgr  28577  upgrres  28594  umgrres  28595  vtxdun  28769  upgrewlkle2  28894  eupthvdres  29519  cycpmfvlem  32302  cycpmfv3  32305  sitgf  33377  cardpred  34124  nummin  34125  bj-gabima  35868  gneispace  42933  gneispacef2  42935  funimaeq  43998  limsupresxr  44530  liminfresxr  44531  funcoressn  45800