rabss2

Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Step	Hyp	Ref	Expression
1		pm3.45	$⊢ (x \in A \to x \in B) \to ((x \in A \land φ) \to (x \in B \land φ))$
2	1	alimi	$⊢ \forall x (x \in A \to x \in B) \to \forall x ((x \in A \land φ) \to (x \in B \land φ))$
3		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
4		ss2ab	$⊢ \{x \| (x \in A \land φ)\} \subseteq \{x \| (x \in B \land φ)\} \leftrightarrow \forall x ((x \in A \land φ) \to (x \in B \land φ))$
5	2 3 4	3imtr4i	$⊢ A \subseteq B \to \{x \| (x \in A \land φ)\} \subseteq \{x \| (x \in B \land φ)\}$
6		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
7		df-rab	$⊢ \{x \in B \| φ\} = \{x \| (x \in B \land φ)\}$
8	5 6 7	3sstr4g	$⊢ A \subseteq B \to \{x \in A \| φ\} \subseteq \{x \in B \| φ\}$

Metamath Proof Explorer