Theorem ralab

Description: Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024)

	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		df-clab	$$⊢x\in \left\{y|\phi \right\}\leftrightarrow \left[x/y\right]\phi$$
4	1	sbievw	$$⊢\left[x/y\right]\phi \leftrightarrow \psi$$
5	3 4	bitri	$$⊢x\in \left\{y|\phi \right\}\leftrightarrow \psi$$
6	5	imbi1i	$$⊢\left(x\in \left\{y|\phi \right\}\to \chi \right)\leftrightarrow \left(\psi \to \chi \right)$$
7		biid	$$⊢\left(\psi \to \chi \right)\leftrightarrow \left(\psi \to \chi \right)$$
8	6 7	bitri	$$⊢\left(x\in \left\{y|\phi \right\}\to \chi \right)\leftrightarrow \left(\psi \to \chi \right)$$
9	8	albii	$$⊢\forall x\left(x\in \left\{y|\phi \right\}\to \chi \right)\leftrightarrow \forall x\left(\psi \to \chi \right)$$
10	2 9	bitri	$$⊢\forall x\in \left\{y|\phi \right\}\chi \leftrightarrow \forall x\left(\psi \to \chi \right)$$