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

Metamath Proof Explorer

Theorem rabss2

Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid axioms. (Revised by TM, 1-Feb-2026)

		Ref	Expression
	Assertion	rabss2	$⊢ A \subseteq B \to \{x \in A \| φ\} \subseteq \{x \in B \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	anim1d	$⊢ A \subseteq B \to ((x \in A \land φ) \to (x \in B \land φ))$
3	2	ss2abdv	$⊢ A \subseteq B \to \{x \| (x \in A \land φ)\} \subseteq \{x \| (x \in B \land φ)\}$
4		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
5		df-rab	$⊢ \{x \in B \| φ\} = \{x \| (x \in B \land φ)\}$
6	3 4 5	3sstr4g	$⊢ A \subseteq B \to \{x \in A \| φ\} \subseteq \{x \in B \| φ\}$