This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \subseteq B \land B \in C) \to A \in V$

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