ssrab

Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006)

		Ref	Expression
	Assertion	ssrab	$⊢ B \subseteq \{x \in A \| φ\} \leftrightarrow (B \subseteq A \land \forall x \in B φ)$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2	1	sseq2i	$⊢ B \subseteq \{x \in A \| φ\} \leftrightarrow B \subseteq \{x \| (x \in A \land φ)\}$
3		ssab	$⊢ B \subseteq \{x \| (x \in A \land φ)\} \leftrightarrow \forall x (x \in B \to (x \in A \land φ))$
4		dfss3	$⊢ B \subseteq A \leftrightarrow \forall x \in B x \in A$
5	4	anbi1i	$⊢ (B \subseteq A \land \forall x \in B φ) \leftrightarrow (\forall x \in B x \in A \land \forall x \in B φ)$
6		r19.26	$⊢ \forall x \in B (x \in A \land φ) \leftrightarrow (\forall x \in B x \in A \land \forall x \in B φ)$
7		df-ral	$⊢ \forall x \in B (x \in A \land φ) \leftrightarrow \forall x (x \in B \to (x \in A \land φ))$
8	5 6 7	3bitr2ri	$⊢ \forall x (x \in B \to (x \in A \land φ)) \leftrightarrow (B \subseteq A \land \forall x \in B φ)$
9	2 3 8	3bitri	$⊢ B \subseteq \{x \in A \| φ\} \leftrightarrow (B \subseteq A \land \forall x \in B φ)$

Metamath Proof Explorer