rabss

Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006)

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

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2	1	sseq1i	$⊢ \{x \in A \| φ\} \subseteq B \leftrightarrow \{x \| (x \in A \land φ)\} \subseteq B$
3		abss	$⊢ \{x \| (x \in A \land φ)\} \subseteq B \leftrightarrow \forall x ((x \in A \land φ) \to x \in B)$
4		impexp	$⊢ ((x \in A \land φ) \to x \in B) \leftrightarrow (x \in A \to (φ \to x \in B))$
5	4	albii	$⊢ \forall x ((x \in A \land φ) \to x \in B) \leftrightarrow \forall x (x \in A \to (φ \to x \in B))$
6		df-ral	$⊢ \forall x \in A (φ \to x \in B) \leftrightarrow \forall x (x \in A \to (φ \to x \in B))$
7	5 6	bitr4i	$⊢ \forall x ((x \in A \land φ) \to x \in B) \leftrightarrow \forall x \in A (φ \to x \in B)$
8	2 3 7	3bitri	$⊢ \{x \in A \| φ\} \subseteq B \leftrightarrow \forall x \in A (φ \to x \in B)$

Metamath Proof Explorer