Theorem ssexgOLD

Description: Obsolete version of ssexg as of 18-Jul-2026. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sseq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵 ) )
2	1	imbi1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ⊆ 𝑥 → 𝐴 ∈ V ) ↔ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V ) ) )
3		vex	⊢ 𝑥 ∈ V
4	3	ssex	⊢ ( 𝐴 ⊆ 𝑥 → 𝐴 ∈ V )
5	2 4	vtoclg	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V ) )
6	5	impcom	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ V )