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

Metamath Proof Explorer

Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Hypothesis axrep4.1 
|- F/ z ph
Assertion axrep4 
|- ( 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 axrep4.1 
 |-  F/ z ph
2 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 ) ) )
3 1 19.3 
 |-  ( A. z ph <-> ph )
4 3 imbi1i 
 |-  ( ( A. z ph -> y = z ) <-> ( ph -> y = z ) )
5 4 albii 
 |-  ( A. y ( A. z ph -> y = z ) <-> A. y ( ph -> y = z ) )
6 5 exbii 
 |-  ( E. z A. y ( A. z ph -> y = z ) <-> E. z A. y ( ph -> y = z ) )
7 6 albii 
 |-  ( A. x E. z A. y ( A. z ph -> y = z ) <-> A. x E. z A. y ( ph -> y = z ) )
8 3 anbi2i 
 |-  ( ( x e. w /\ A. z ph ) <-> ( x e. w /\ ph ) )
9 8 exbii 
 |-  ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) )
10 9 bibi2i 
 |-  ( ( y e. z <-> E. x ( x e. w /\ A. z ph ) ) <-> ( y e. z <-> E. x ( x e. w /\ ph ) ) )
11 10 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 ) ) )
12 11 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 ) ) )
13 2 7 12 3imtr3i 
 |-  ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )