Theorem funfnd 6568

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 6567	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 221	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

This proof depends on syntax axioms:   → wi 4  dom cdm 5659  Fun wfun 6531   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-fn 6540

This theorem is used by:  fncofn  6653  resfunexg  7218  ralima  7240  funiunfv  7249  funelss  8048  funsssuppss  8192  frrlem4  8292  smores2  8347  tfrlem1  8368  resfnfinfin  9308  resfifsupp  9371  ordtypelem4  9497  ordtypelem9  9502  ordtypelem10  9503  brdom3  10535  brdom5  10536  brdom4  10537  fpwwe2lem10  10653  hashimarn  14509  resunimafz0  14514  isstruct2  17247  invf  17863  lindfrn  22040  psdmul  22400  ofco2  22679  dfac14  23850  perfdvf  26137  c1lip2  26232  taylf  26604  elno2  27898  noinfbnd2lem1  27974  noetainflem4  27984  lpvtx  29533  upgrle2  29570  uhgrvtxedgiedgb  29601  uhgr2edg  29676  ushgredgedg  29697  ushgredgedgloop  29699  subgruhgredgd  29752  subuhgr  29754  subupgr  29755  subumgr  29756  subusgr  29757  upgrres  29774  umgrres  29775  vtxdun  29949  upgrewlkle2  30074  eupthvdres  30723  cycpmfvlem  33560  cycpmfv3  33563  sitgf  34866  cardpred  35605  nummin  35606  bj-gabima  37692  gneispace  44982  gneispacef2  44984  funimaeq  46083  limsupresxr  46602  liminfresxr  46603  funcoressn  47938  isubgr0uhgr  48797  upgrimwlklem1  48821