Theorem ralrab2

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

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

Proof

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