Theorem funfnd

Description: A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypothesis	funfnd.1	⊢ ( 𝜑 → Fun 𝐴 )
Assertion	funfnd	⊢ ( 𝜑 → 𝐴 Fn dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		funfnd.1	⊢ ( 𝜑 → Fun 𝐴 )
2		funfn	⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
3	1 2	sylib	⊢ ( 𝜑 → 𝐴 Fn dom 𝐴 )