Theorem ssexg

Description: A subclass of a set is a set. Exercise 3 of TakeutiZaring p. 22 (generalized). (Contributed by NM, 14-Aug-1994) (Proof shortened by BJ, 18-Jul-2026)

	Ref	Expression
Assertion	ssexg	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
2		inex2g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ∩ 𝐵 ) ∈ V )
3		eleq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∈ V ↔ 𝐴 ∈ V ) )
4	3	biimpa	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ∈ V ) → 𝐴 ∈ V )
5	2 4	sylan2	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ V )
6	1 5	sylanb	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ V )