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

Metamath Proof Explorer

Theorem axrep4v

Description: Version of axrep4 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep4v 
|- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 ax-rep 
 |-  ( A. x E. z A. y ( A. z ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) )
2 19.3v 
 |-  ( A. z ph <-> ph )
3 2 imbi1i 
 |-  ( ( A. z ph -> y = z ) <-> ( ph -> y = z ) )
4 3 albii 
 |-  ( A. y ( A. z ph -> y = z ) <-> A. y ( ph -> y = z ) )
5 4 exbii 
 |-  ( E. z A. y ( A. z ph -> y = z ) <-> E. z A. y ( ph -> y = z ) )
6 5 albii 
 |-  ( A. x E. z A. y ( A. z ph -> y = z ) <-> A. x E. z A. y ( ph -> y = z ) )
7 2 anbi2i 
 |-  ( ( x e. w /\ A. z ph ) <-> ( x e. w /\ ph ) )
8 7 exbii 
 |-  ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) )
9 8 bibi2i 
 |-  ( ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> ( y e. z <-> E. x ( x e. w /\ ph ) ) )
10 9 albii 
 |-  ( A. y ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
11 10 exbii 
 |-  ( E. z A. y ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
12 1 6 11 3imtr3i 
 |-  ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )