Theorem fssdmd

Description: Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, deduction form. (Contributed by AV, 21-Aug-2022)

	Ref	Expression
Hypotheses	fssdmd.f	$$⊢\phi \to F:A⟶B$$
	fssdmd.d	$$⊢\phi \to D\subseteq \mathrm{dom}F$$
Assertion	fssdmd	$$⊢\phi \to D\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		fssdmd.f	$$⊢\phi \to F:A⟶B$$
2		fssdmd.d	$$⊢\phi \to D\subseteq \mathrm{dom}F$$
3	1	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
4	2 3	sseqtrd	$$⊢\phi \to D\subseteq A$$