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

Metamath Proof Explorer

Theorem axrep6OLD

Description: Obsolete version of axrep6 as of 18-Sep-2025. (Contributed by SN, 18-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-rep 
 |-  ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
2 df-mo 
 |-  ( E* z ph <-> E. y A. z ( ph -> z = y ) )
3 19.3v 
 |-  ( A. y ph <-> ph )
4 3 imbi1i 
 |-  ( ( A. y ph -> z = y ) <-> ( ph -> z = y ) )
5 4 albii 
 |-  ( A. z ( A. y ph -> z = y ) <-> A. z ( ph -> z = y ) )
6 5 exbii 
 |-  ( E. y A. z ( A. y ph -> z = y ) <-> E. y A. z ( ph -> z = y ) )
7 2 6 bitr4i 
 |-  ( E* z ph <-> E. y A. z ( A. y ph -> z = y ) )
8 7 albii 
 |-  ( A. w E* z ph <-> A. w E. y A. z ( A. y ph -> z = y ) )
9 3 rexbii 
 |-  ( E. w e. x A. y ph <-> E. w e. x ph )
10 df-rex 
 |-  ( E. w e. x A. y ph <-> E. w ( w e. x /\ A. y ph ) )
11 9 10 bitr3i 
 |-  ( E. w e. x ph <-> E. w ( w e. x /\ A. y ph ) )
12 11 bibi2i 
 |-  ( ( z e. y <-> E. w e. x ph ) <-> ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
13 12 albii 
 |-  ( A. z ( z e. y <-> E. w e. x ph ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
14 13 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 /\ A. y ph ) ) )
15 1 8 14 3imtr4i 
 |-  ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )