Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		dfss2	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
2		inex2g	$⊢ B \in C \to A \cap B \in V$
3		eleq1	$⊢ A \cap B = A \to (A \cap B \in V \leftrightarrow A \in V)$
4	3	biimpa	$⊢ (A \cap B = A \land A \cap B \in V) \to A \in V$
5	2 4	sylan2	$⊢ (A \cap B = A \land B \in C) \to A \in V$
6	1 5	sylanb	$⊢ (A \subseteq B \land B \in C) \to A \in V$