ralrab

Description: Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010)

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

Step	Hyp	Ref	Expression
1		ralab.1	$⊢ y = x \to (φ \leftrightarrow ψ)$
2	1	elrab	$⊢ x \in \{y \in A \| φ\} \leftrightarrow (x \in A \land ψ)$
3	2	imbi1i	$⊢ (x \in \{y \in A \| φ\} \to χ) \leftrightarrow ((x \in A \land ψ) \to χ)$
4		impexp	$⊢ ((x \in A \land ψ) \to χ) \leftrightarrow (x \in A \to (ψ \to χ))$
5	3 4	bitri	$⊢ (x \in \{y \in A \| φ\} \to χ) \leftrightarrow (x \in A \to (ψ \to χ))$
6	5	ralbii2	$⊢ \forall x \in \{y \in A \| φ\} χ \leftrightarrow \forall x \in A (ψ \to χ)$

Metamath Proof Explorer