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

Metamath Proof Explorer

Theorem rabssab

Description: A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016)

		Ref	Expression
	Assertion	rabssab	$⊢ \{x \in A \| φ\} \subseteq \{x \| φ\}$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		simpr	$⊢ (x \in A \land φ) \to φ$
3	2	ss2abi	$⊢ \{x \| (x \in A \land φ)\} \subseteq \{x \| φ\}$
4	1 3	eqsstri	$⊢ \{x \in A \| φ\} \subseteq \{x \| φ\}$