Theorem ralab

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

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

Proof

Step	Hyp	Ref	Expression
1		ralab.1	$$⊢y=x\to \left(\phi \leftrightarrow \psi \right)$$
2		df-ral	$$⊢\forall x\in \left\{y|\phi \right\}\chi \leftrightarrow \forall x\left(x\in \left\{y|\phi \right\}\to \chi \right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3 1	elab	$$⊢x\in \left\{y|\phi \right\}\leftrightarrow \psi$$
5	4	imbi1i	$$⊢\left(x\in \left\{y|\phi \right\}\to \chi \right)\leftrightarrow \left(\psi \to \chi \right)$$
6	5	albii	$$⊢\forall x\left(x\in \left\{y|\phi \right\}\to \chi \right)\leftrightarrow \forall x\left(\psi \to \chi \right)$$
7	2 6	bitri	$$⊢\forall x\in \left\{y|\phi \right\}\chi \leftrightarrow \forall x\left(\psi \to \chi \right)$$