Theorem axrep6g

Description: axrep6 in class notation. It is equivalent to both ax-rep and abrexexg , providing a direct link between the two. (Contributed by SN, 11-Dec-2024)

	Ref	Expression
Assertion	axrep6g	$$⊢\left(A\in V\wedge \forall x{\exists }^{*}y\psi \right)\to \left\{y|\exists x\in A\psi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rexeq	$$⊢z=A\to \left(\exists x\in z\psi \leftrightarrow \exists x\in A\psi \right)$$
2	1	abbidv	$$⊢z=A\to \left\{y|\exists x\in z\psi \right\}=\left\{y|\exists x\in A\psi \right\}$$
3	2	eleq1d	$$⊢z=A\to \left(\left\{y|\exists x\in z\psi \right\}\in \mathrm{V}\leftrightarrow \left\{y|\exists x\in A\psi \right\}\in \mathrm{V}\right)$$
4	3	imbi2d	$$⊢z=A\to \left(\left(\forall x{\exists }^{*}y\psi \to \left\{y|\exists x\in z\psi \right\}\in \mathrm{V}\right)\leftrightarrow \left(\forall x{\exists }^{*}y\psi \to \left\{y|\exists x\in A\psi \right\}\in \mathrm{V}\right)\right)$$
5		axrep6	$$⊢\forall x{\exists }^{*}y\psi \to \exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\psi \right)$$
6		abbi	$$⊢\forall y\left(y\in w\leftrightarrow \exists x\in z\psi \right)\to \left\{y|y\in w\right\}=\left\{y|\exists x\in z\psi \right\}$$
7		abid2	$$⊢\left\{y|y\in w\right\}=w$$
8		vex	$$⊢w\in \mathrm{V}$$
9	7 8	eqeltri	$$⊢\left\{y|y\in w\right\}\in \mathrm{V}$$
10	6 9	eqeltrrdi	$$⊢\forall y\left(y\in w\leftrightarrow \exists x\in z\psi \right)\to \left\{y|\exists x\in z\psi \right\}\in \mathrm{V}$$
11	10	exlimiv	$$⊢\exists w\forall y\left(y\in w\leftrightarrow \exists x\in z\psi \right)\to \left\{y|\exists x\in z\psi \right\}\in \mathrm{V}$$
12	5 11	syl	$$⊢\forall x{\exists }^{*}y\psi \to \left\{y|\exists x\in z\psi \right\}\in \mathrm{V}$$
13	4 12	vtoclg	$$⊢A\in V\to \left(\forall x{\exists }^{*}y\psi \to \left\{y|\exists x\in A\psi \right\}\in \mathrm{V}\right)$$
14	13	imp	$$⊢\left(A\in V\wedge \forall x{\exists }^{*}y\psi \right)\to \left\{y|\exists x\in A\psi \right\}\in \mathrm{V}$$