Theorem ffdmd

Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	ffdmd.1	$$⊢\phi \to F:A⟶B$$
Assertion	ffdmd	$$⊢\phi \to F:\mathrm{dom}F⟶B$$

Proof

Step	Hyp	Ref	Expression
1		ffdmd.1	$$⊢\phi \to F:A⟶B$$
2		ffdm	$$⊢F:A⟶B\to \left(F:\mathrm{dom}F⟶B\wedge \mathrm{dom}F\subseteq A\right)$$
3	1 2	syl	$$⊢\phi \to \left(F:\mathrm{dom}F⟶B\wedge \mathrm{dom}F\subseteq A\right)$$
4	3	simpld	$$⊢\phi \to F:\mathrm{dom}F⟶B$$