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	$$⊢\left(A\subseteq B\wedge B\in C\right)\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢x=B\to \left(A\subseteq x\leftrightarrow A\subseteq B\right)$$
2	1	imbi1d	$$⊢x=B\to \left(\left(A\subseteq x\to A\in \mathrm{V}\right)\leftrightarrow \left(A\subseteq B\to A\in \mathrm{V}\right)\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	ssex	$$⊢A\subseteq x\to A\in \mathrm{V}$$
5	2 4	vtoclg	$$⊢B\in C\to \left(A\subseteq B\to A\in \mathrm{V}\right)$$
6	5	impcom	$$⊢\left(A\subseteq B\wedge B\in C\right)\to A\in \mathrm{V}$$