Theorem ralrab

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

	Ref	Expression
Hypothesis	ralab.1	$$⊢y=x\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralrab	$$⊢\forall x\in \left\{y\in A|\phi \right\}\chi \leftrightarrow \forall x\in A\left(\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralab.1	$$⊢y=x\to \left(\phi \leftrightarrow \psi \right)$$
2	1	elrab	$$⊢x\in \left\{y\in A|\phi \right\}\leftrightarrow \left(x\in A\wedge \psi \right)$$
3	2	imbi1i	$$⊢\left(x\in \left\{y\in A|\phi \right\}\to \chi \right)\leftrightarrow \left(\left(x\in A\wedge \psi \right)\to \chi \right)$$
4		impexp	$$⊢\left(\left(x\in A\wedge \psi \right)\to \chi \right)\leftrightarrow \left(x\in A\to \left(\psi \to \chi \right)\right)$$
5	3 4	bitri	$$⊢\left(x\in \left\{y\in A|\phi \right\}\to \chi \right)\leftrightarrow \left(x\in A\to \left(\psi \to \chi \right)\right)$$
6	5	ralbii2	$$⊢\forall x\in \left\{y\in A|\phi \right\}\chi \leftrightarrow \forall x\in A\left(\psi \to \chi \right)$$