Theorem ralab2

Description: Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
2		df-ral	$$⊢\forall x\in \left\{y|\phi \right\}\psi \leftrightarrow \forall x\left(x\in \left\{y|\phi \right\}\to \psi \right)$$
3		nfsab1	$$⊢Ⅎyx\in \left\{y|\phi \right\}$$
4		nfv	$$⊢Ⅎy\psi$$
5	3 4	nfim	$$⊢Ⅎy\left(x\in \left\{y|\phi \right\}\to \psi \right)$$
6		nfv	$$⊢Ⅎx\left(\phi \to \chi \right)$$
7		eleq1ab	$$⊢x=y\to \left(x\in \left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\phi \right\}\right)$$
8		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
9	7 8	bitrdi	$$⊢x=y\to \left(x\in \left\{y|\phi \right\}\leftrightarrow \phi \right)$$
10	9 1	imbi12d	$$⊢x=y\to \left(\left(x\in \left\{y|\phi \right\}\to \psi \right)\leftrightarrow \left(\phi \to \chi \right)\right)$$
11	5 6 10	cbvalv1	$$⊢\forall x\left(x\in \left\{y|\phi \right\}\to \psi \right)\leftrightarrow \forall y\left(\phi \to \chi \right)$$
12	2 11	bitri	$$⊢\forall x\in \left\{y|\phi \right\}\psi \leftrightarrow \forall y\left(\phi \to \chi \right)$$