Metamath Proof Explorer

Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep6 
|- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )

Proof

Step Hyp Ref Expression
1 axrep4v 
 |-  ( A. w E. y A. z ( ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ ph ) ) )
2 df-mo 
 |-  ( E* z ph <-> E. y A. z ( ph -> z = y ) )
3 2 albii 
 |-  ( A. w E* z ph <-> A. w E. y A. z ( ph -> z = y ) )
4 df-rex 
 |-  ( E. w e. x ph <-> E. w ( w e. x /\ ph ) )
5 4 bibi2i 
 |-  ( ( z e. y <-> E. w e. x ph ) <-> ( z e. y <-> E. w ( w e. x /\ ph ) ) )
6 5 albii 
 |-  ( A. z ( z e. y <-> E. w e. x ph ) <-> A. z ( z e. y <-> E. w ( w e. x /\ ph ) ) )
7 6 exbii 
 |-  ( E. y A. z ( z e. y <-> E. w e. x ph ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ ph ) ) )
8 1 3 7 3imtr4i 
 |-  ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )