This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )