Theorem funfnd

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

	Ref	Expression
Hypothesis	funfnd.1	$$⊢\phi \to \mathrm{Fun}A$$
Assertion	funfnd	$$⊢\phi \to AFn\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		funfnd.1	$$⊢\phi \to \mathrm{Fun}A$$
2		funfn	$$⊢\mathrm{Fun}A\leftrightarrow AFn\mathrm{dom}A$$
3	1 2	sylib	$$⊢\phi \to AFn\mathrm{dom}A$$