Theorem ssexg

Description: The subset of a set is also a set. Exercise 3 of TakeutiZaring p. 22 (generalized). (Contributed by NM, 14-Aug-1994)

	Ref	Expression
Assertion	ssexg	$$⊢\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}$$