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

Metamath Proof Explorer

Theorem ssrab3

Description: Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

		Ref	Expression
	Hypothesis	ssrab3.1	$⊢ B = \{x \in A \| φ\}$
	Assertion	ssrab3	$⊢ B \subseteq A$

Step	Hyp	Ref	Expression
1		ssrab3.1	$⊢ B = \{x \in A \| φ\}$
2		ssrab2	$⊢ \{x \in A \| φ\} \subseteq A$
3	1 2	eqsstri	$⊢ B \subseteq A$