Theorem funfnd 6366

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

Syntax hints:   → wi 4  dom cdm 5524  Fun wfun 6329   Fn wfn 6330

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-fn 6338

This theorem is referenced by:  resfunexg  6969  funiunfv  6999  funelss  7750  funsssuppss  7864  wfrlem4  7968  smores2  8001  tfrlem1  8022  resfnfinfin  8837  resfifsupp  8894  ordtypelem4  9018  ordtypelem9  9023  ordtypelem10  9024  brdom3  9988  brdom5  9989  brdom4  9990  fpwwe2lem10  10100  hashimarn  13851  resunimafz0  13853  isstruct2  16551  invf  17097  lindfrn  20586  ofco2  21151  dfac14  22318  perfdvf  24602  c1lip2  24697  taylf  25055  lpvtx  26960  upgrle2  26997  uhgrvtxedgiedgb  27028  uhgr2edg  27097  ushgredgedg  27118  ushgredgedgloop  27120  subgruhgredgd  27173  subuhgr  27175  subupgr  27176  subumgr  27177  subusgr  27178  upgrres  27195  umgrres  27196  vtxdun  27370  upgrewlkle2  27495  eupthvdres  28119  cycpmfvlem  30905  cycpmfv3  30908  sitgf  31833  cardpred  32591  nummin  32592  frrlem4  33387  elno2  33422  noinfbnd2lem1  33498  noetainflem4  33508  gneispace  41210  gneispacef2  41212  funimaeq  42252  limsupresxr  42774  liminfresxr  42775  funcoressn  44000