Theorem funfnd 5357

Description: A function is a function over 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 5356	. 2 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐴 Fn dom 𝐴)

Syntax hints:   → wi 4  dom cdm 4725  Fun wfun 5320   Fn wfn 5321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5329

This theorem is referenced by:  fncofn  5832  ccatalpha  11194  ennnfonelemf1  13044  dvfgg  15418  lpvtx  15936  uhgrvtxedgiedgb  16000  uhgr2edg  16063  ushgredgedg  16083  ushgredgedgloop  16085  subgruhgredgdm  16127  subuhgr  16129  subupgr  16130  subumgr  16131  subusgr  16132  vtxdfifiun  16154  trlsegvdegfi  16324  eupth2lem3lem2fi  16326  eupth2lem3lem6fi  16328  eupth2lem3lem4fi  16330  eupthvdres  16332