Theorem fssdm

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

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

Proof

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