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 ) ) ) )