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	|- ( ( A e. V /\ A. x E* y ps ) -> { y | E. x e. A ps } e. _V )

Proof

Step	Hyp	Ref	Expression
1		rexeq	|- ( z = A -> ( E. x e. z ps <-> E. x e. A ps ) )
2	1	abbidv	|- ( z = A -> { y | E. x e. z ps } = { y | E. x e. A ps } )
3	2	eleq1d	|- ( z = A -> ( { y | E. x e. z ps } e. _V <-> { y | E. x e. A ps } e. _V ) )
4	3	imbi2d	|- ( z = A -> ( ( A. x E* y ps -> { y | E. x e. z ps } e. _V ) <-> ( A. x E* y ps -> { y | E. x e. A ps } e. _V ) ) )
5		axrep6	|- ( A. x E* y ps -> E. w A. y ( y e. w <-> E. x e. z ps ) )
6		abbi	|- ( A. y ( y e. w <-> E. x e. z ps ) -> { y | y e. w } = { y | E. x e. z ps } )
7		abid2	|- { y | y e. w } = w
8		vex	|- w e. _V
9	7 8	eqeltri	|- { y | y e. w } e. _V
10	6 9	eqeltrrdi	|- ( A. y ( y e. w <-> E. x e. z ps ) -> { y | E. x e. z ps } e. _V )
11	10	exlimiv	|- ( E. w A. y ( y e. w <-> E. x e. z ps ) -> { y | E. x e. z ps } e. _V )
12	5 11	syl	|- ( A. x E* y ps -> { y | E. x e. z ps } e. _V )
13	4 12	vtoclg	|- ( A e. V -> ( A. x E* y ps -> { y | E. x e. A ps } e. _V ) )
14	13	imp	|- ( ( A e. V /\ A. x E* y ps ) -> { y | E. x e. A ps } e. _V )