ralrab2

Description: Universal quantification over a restricted class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Hypothesis	ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
	Assertion	ralrab2	$⊢ \forall x \in \{y \in A \| φ\} ψ \leftrightarrow \forall y \in A (φ \to χ)$

Step	Hyp	Ref	Expression
1		ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
2		df-rab	$⊢ \{y \in A \| φ\} = \{y \| (y \in A \land φ)\}$
3	2	raleqi	$⊢ \forall x \in \{y \in A \| φ\} ψ \leftrightarrow \forall x \in \{y \| (y \in A \land φ)\} ψ$
4	1	ralab2	$⊢ \forall x \in \{y \| (y \in A \land φ)\} ψ \leftrightarrow \forall y ((y \in A \land φ) \to χ)$
5		impexp	$⊢ ((y \in A \land φ) \to χ) \leftrightarrow (y \in A \to (φ \to χ))$
6	5	albii	$⊢ \forall y ((y \in A \land φ) \to χ) \leftrightarrow \forall y (y \in A \to (φ \to χ))$
7		df-ral	$⊢ \forall y \in A (φ \to χ) \leftrightarrow \forall y (y \in A \to (φ \to χ))$
8	6 7	bitr4i	$⊢ \forall y ((y \in A \land φ) \to χ) \leftrightarrow \forall y \in A (φ \to χ)$
9	3 4 8	3bitri	$⊢ \forall x \in \{y \in A \| φ\} ψ \leftrightarrow \forall y \in A (φ \to χ)$

Metamath Proof Explorer