Theorem ssexd

Description: A subclass of a set is a set. Deduction form of ssexg . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ssexd.1	$$⊢\phi \to B\in C$$
	ssexd.2	$$⊢\phi \to A\subseteq B$$
Assertion	ssexd	$$⊢\phi \to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssexd.1	$$⊢\phi \to B\in C$$
2		ssexd.2	$$⊢\phi \to A\subseteq B$$
3		ssexg	$$⊢\left(A\subseteq B\wedge B\in C\right)\to A\in \mathrm{V}$$
4	2 1 3	syl2anc	$$⊢\phi \to A\in \mathrm{V}$$