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	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
	ssexd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ssexd.1	⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
2		ssexd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		ssexg	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ V )
4	2 1 3	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ V )