Metamath Proof Explorer

Theorem axrep1

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet https://us.metamath.org/mmsolitaire/mms.html . Equivalence is shown via the path ax-rep -> axrep1 -> axrep2 -> axrepnd -> zfcndrep = ax-rep . (Contributed by NM, 19-Nov-2005) (Proof shortened by Mario Carneiro, 17-Nov-2016) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

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

Proof

Step Hyp Ref Expression
1 elequ2 
 |-  ( w = y -> ( x e. w <-> x e. y ) )
2 1 anbi1d 
 |-  ( w = y -> ( ( x e. w /\ ph ) <-> ( x e. y /\ ph ) ) )
3 2 exbidv 
 |-  ( w = y -> ( E. x ( x e. w /\ ph ) <-> E. x ( x e. y /\ ph ) ) )
4 3 bibi2d 
 |-  ( w = y -> ( ( z e. x <-> E. x ( x e. w /\ ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ ph ) ) ) )
5 4 albidv 
 |-  ( w = y -> ( A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) ) )
6 5 exbidv 
 |-  ( w = y -> ( E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) <-> E. x A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) ) )
7 6 imbi2d 
 |-  ( w = y -> ( ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) ) <-> ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) ) ) )
8 ax-rep 
 |-  ( A. x E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) )
9 19.3v 
 |-  ( A. y ph <-> ph )
10 9 imbi1i 
 |-  ( ( A. y ph -> z = y ) <-> ( ph -> z = y ) )
11 10 albii 
 |-  ( A. z ( A. y ph -> z = y ) <-> A. z ( ph -> z = y ) )
12 11 exbii 
 |-  ( E. y A. z ( A. y ph -> z = y ) <-> E. y A. z ( ph -> z = y ) )
13 12 albii 
 |-  ( A. x E. y A. z ( A. y ph -> z = y ) <-> A. x E. y A. z ( ph -> z = y ) )
14 nfv 
 |-  F/ x z e. y
15 nfe1 
 |-  F/ x E. x ( x e. w /\ A. y ph )
16 14 15 nfbi 
 |-  F/ x ( z e. y <-> E. x ( x e. w /\ A. y ph ) )
17 16 nfal 
 |-  F/ x A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) )
18 nfv 
 |-  F/ y A. z ( z e. x <-> E. x ( x e. w /\ ph ) )
19 elequ2 
 |-  ( y = x -> ( z e. y <-> z e. x ) )
20 9 anbi2i 
 |-  ( ( x e. w /\ A. y ph ) <-> ( x e. w /\ ph ) )
21 20 exbii 
 |-  ( E. x ( x e. w /\ A. y ph ) <-> E. x ( x e. w /\ ph ) )
22 21 a1i 
 |-  ( y = x -> ( E. x ( x e. w /\ A. y ph ) <-> E. x ( x e. w /\ ph ) ) )
23 19 22 bibi12d 
 |-  ( y = x -> ( ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) <-> ( z e. x <-> E. x ( x e. w /\ ph ) ) ) )
24 23 albidv 
 |-  ( y = x -> ( A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) <-> A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) ) )
25 17 18 24 cbvexv1 
 |-  ( E. y A. z ( z e. y <-> E. x ( x e. w /\ A. y ph ) ) <-> E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) )
26 8 13 25 3imtr3i 
 |-  ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. w /\ ph ) ) )
27 7 26 chvarvv 
 |-  ( A. x E. y A. z ( ph -> z = y ) -> E. x A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) )
28 27 19.35ri 
 |-  E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) )