Theorem funfnd 6579

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

Syntax hints:   → wi 4  dom cdm 5676  Fun wfun 6537   Fn wfn 6538

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6546

This theorem is referenced by:  fncofn  6666  resfunexg  7216  funiunfv  7246  funelss  8032  funsssuppss  8174  frrlem4  8273  wfrlem4OLD  8311  smores2  8353  tfrlem1  8375  resfnfinfin  9331  resfifsupp  9391  ordtypelem4  9515  ordtypelem9  9520  ordtypelem10  9521  brdom3  10522  brdom5  10523  brdom4  10524  fpwwe2lem10  10634  hashimarn  14399  resunimafz0  14403  isstruct2  17081  invf  17714  lindfrn  21375  ofco2  21952  dfac14  23121  perfdvf  25419  c1lip2  25514  taylf  25872  elno2  27154  noinfbnd2lem1  27230  noetainflem4  27240  lpvtx  28325  upgrle2  28362  uhgrvtxedgiedgb  28393  uhgr2edg  28462  ushgredgedg  28483  ushgredgedgloop  28485  subgruhgredgd  28538  subuhgr  28540  subupgr  28541  subumgr  28542  subusgr  28543  upgrres  28560  umgrres  28561  vtxdun  28735  upgrewlkle2  28860  eupthvdres  29485  cycpmfvlem  32266  cycpmfv3  32269  sitgf  33341  cardpred  34088  nummin  34089  bj-gabima  35815  gneispace  42875  gneispacef2  42877  funimaeq  43940  limsupresxr  44472  liminfresxr  44473  funcoressn  45742