Theorem ssexi

Description: A subclass of a set is a set. (Contributed by NM, 9-Sep-1993)

	Ref	Expression
Hypotheses	ssexi.1	⊢ 𝐵 ∈ V
	ssexi.2	⊢ 𝐴 ⊆ 𝐵
Assertion	ssexi	⊢ 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		ssexi.1	⊢ 𝐵 ∈ V
2		ssexi.2	⊢ 𝐴 ⊆ 𝐵
3	1	ssex	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )
4	2 3	ax-mp	⊢ 𝐴 ∈ V