Theorem ralabOLD

Description: Obsolete version of ralab as of 2-Nov-2024. (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ralab.1	$$⊢y=x\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralabOLD	$$⊢\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)$$