Metamath Proof Explorer

Theorem rabss2OLD

Description: Obsolete version of rabss2 as of 1-Feb-2026. (Contributed by NM, 30-May-2006) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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 \| φ\}$