ss2rab

Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999)

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

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		df-rab	$⊢ \{x \in A \| ψ\} = \{x \| (x \in A \land ψ)\}$
3	1 2	sseq12i	$⊢ \{x \in A \| φ\} \subseteq \{x \in A \| ψ\} \leftrightarrow \{x \| (x \in A \land φ)\} \subseteq \{x \| (x \in A \land ψ)\}$
4		ss2ab	$⊢ \{x \| (x \in A \land φ)\} \subseteq \{x \| (x \in A \land ψ)\} \leftrightarrow \forall x ((x \in A \land φ) \to (x \in A \land ψ))$
5		df-ral	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow \forall x (x \in A \to (φ \to ψ))$
6		imdistan	$⊢ (x \in A \to (φ \to ψ)) \leftrightarrow ((x \in A \land φ) \to (x \in A \land ψ))$
7	6	albii	$⊢ \forall x (x \in A \to (φ \to ψ)) \leftrightarrow \forall x ((x \in A \land φ) \to (x \in A \land ψ))$
8	5 7	bitr2i	$⊢ \forall x ((x \in A \land φ) \to (x \in A \land ψ)) \leftrightarrow \forall x \in A (φ \to ψ)$
9	3 4 8	3bitri	$⊢ \{x \in A \| φ\} \subseteq \{x \in A \| ψ\} \leftrightarrow \forall x \in A (φ \to ψ)$

Metamath Proof Explorer