Theorem funfnd

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

	Ref	Expression
Hypothesis	funfnd.1	|- ( ph -> Fun A )
Assertion	funfnd	|- ( ph -> A Fn dom A )

Proof

Step	Hyp	Ref	Expression
1		funfnd.1	|- ( ph -> Fun A )
2		funfn	|- ( Fun A <-> A Fn dom A )
3	1 2	sylib	|- ( ph -> A Fn dom A )