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	|- ( ph -> B e. C )
	ssexd.2	|- ( ph -> A C_ B )
Assertion	ssexd	|- ( ph -> A e. _V )

Proof

Step	Hyp	Ref	Expression
1		ssexd.1	|- ( ph -> B e. C )
2		ssexd.2	|- ( ph -> A C_ B )
3		ssexg	|- ( ( A C_ B /\ B e. C ) -> A e. _V )
4	2 1 3	syl2anc	|- ( ph -> A e. _V )