Metamath Proof Explorer

Theorem axrepndlem1

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axrep2 
 |-  E. x ( E. y A. w ( [ w / z ] ph -> w = y ) -> A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) )
2 nfnae 
 |-  F/ x -. A. y y = z
3 nfnae 
 |-  F/ y -. A. y y = z
4 nfnae 
 |-  F/ z -. A. y y = z
5 nfs1v 
 |-  F/ z [ w / z ] ph
6 5 a1i 
 |-  ( -. A. y y = z -> F/ z [ w / z ] ph )
7 nfcvd 
 |-  ( -. A. y y = z -> F/_ z w )
8 nfcvf2 
 |-  ( -. A. y y = z -> F/_ z y )
9 7 8 nfeqd 
 |-  ( -. A. y y = z -> F/ z w = y )
10 6 9 nfimd 
 |-  ( -. A. y y = z -> F/ z ( [ w / z ] ph -> w = y ) )
11 sbequ12r 
 |-  ( w = z -> ( [ w / z ] ph <-> ph ) )
12 equequ1 
 |-  ( w = z -> ( w = y <-> z = y ) )
13 11 12 imbi12d 
 |-  ( w = z -> ( ( [ w / z ] ph -> w = y ) <-> ( ph -> z = y ) ) )
14 13 a1i 
 |-  ( -. A. y y = z -> ( w = z -> ( ( [ w / z ] ph -> w = y ) <-> ( ph -> z = y ) ) ) )
15 4 10 14 cbvald 
 |-  ( -. A. y y = z -> ( A. w ( [ w / z ] ph -> w = y ) <-> A. z ( ph -> z = y ) ) )
16 3 15 exbid 
 |-  ( -. A. y y = z -> ( E. y A. w ( [ w / z ] ph -> w = y ) <-> E. y A. z ( ph -> z = y ) ) )
17 nfvd 
 |-  ( -. A. y y = z -> F/ z w e. x )
18 8 nfcrd 
 |-  ( -. A. y y = z -> F/ z x e. y )
19 3 6 nfald 
 |-  ( -. A. y y = z -> F/ z A. y [ w / z ] ph )
20 18 19 nfand 
 |-  ( -. A. y y = z -> F/ z ( x e. y /\ A. y [ w / z ] ph ) )
21 2 20 nfexd 
 |-  ( -. A. y y = z -> F/ z E. x ( x e. y /\ A. y [ w / z ] ph ) )
22 17 21 nfbid 
 |-  ( -. A. y y = z -> F/ z ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) )
23 elequ1 
 |-  ( w = z -> ( w e. x <-> z e. x ) )
24 23 adantl 
 |-  ( ( -. A. y y = z /\ w = z ) -> ( w e. x <-> z e. x ) )
25 nfeqf2 
 |-  ( -. A. y y = z -> F/ y w = z )
26 3 25 nfan1 
 |-  F/ y ( -. A. y y = z /\ w = z )
27 11 adantl 
 |-  ( ( -. A. y y = z /\ w = z ) -> ( [ w / z ] ph <-> ph ) )
28 26 27 albid 
 |-  ( ( -. A. y y = z /\ w = z ) -> ( A. y [ w / z ] ph <-> A. y ph ) )
29 28 anbi2d 
 |-  ( ( -. A. y y = z /\ w = z ) -> ( ( x e. y /\ A. y [ w / z ] ph ) <-> ( x e. y /\ A. y ph ) ) )
30 29 exbidv 
 |-  ( ( -. A. y y = z /\ w = z ) -> ( E. x ( x e. y /\ A. y [ w / z ] ph ) <-> E. x ( x e. y /\ A. y ph ) ) )
31 24 30 bibi12d 
 |-  ( ( -. A. y y = z /\ w = z ) -> ( ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
32 31 ex 
 |-  ( -. A. y y = z -> ( w = z -> ( ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) <-> ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
33 4 22 32 cbvald 
 |-  ( -. A. y y = z -> ( A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) <-> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
34 16 33 imbi12d 
 |-  ( -. A. y y = z -> ( ( E. y A. w ( [ w / z ] ph -> w = y ) -> A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) ) <-> ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
35 2 34 exbid 
 |-  ( -. A. y y = z -> ( E. x ( E. y A. w ( [ w / z ] ph -> w = y ) -> A. w ( w e. x <-> E. x ( x e. y /\ A. y [ w / z ] ph ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) ) )
36 1 35 mpbii 
 |-  ( -. A. y y = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )