Metamath Proof Explorer


Theorem axpowndlem4

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Proof shortened by Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion axpowndlem4
|- ( -. A. y y = x -> ( -. A. y y = z -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )

Proof

Step Hyp Ref Expression
1 axpowndlem3
 |-  ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
2 1 ax-gen
 |-  A. w ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
3 nfnae
 |-  F/ y -. A. y y = x
4 nfnae
 |-  F/ y -. A. y y = z
5 3 4 nfan
 |-  F/ y ( -. A. y y = x /\ -. A. y y = z )
6 nfcvf
 |-  ( -. A. y y = x -> F/_ y x )
7 6 adantr
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y x )
8 nfcvd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y w )
9 7 8 nfeqd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x = w )
10 9 nfnd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y -. x = w )
11 nfnae
 |-  F/ x -. A. y y = x
12 nfnae
 |-  F/ x -. A. y y = z
13 11 12 nfan
 |-  F/ x ( -. A. y y = x /\ -. A. y y = z )
14 nfv
 |-  F/ w ( -. A. y y = x /\ -. A. y y = z )
15 nfnae
 |-  F/ z -. A. y y = x
16 nfnae
 |-  F/ z -. A. y y = z
17 15 16 nfan
 |-  F/ z ( -. A. y y = x /\ -. A. y y = z )
18 7 8 nfeld
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. w )
19 17 18 nfexd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. z x e. w )
20 nfcvf
 |-  ( -. A. y y = z -> F/_ y z )
21 20 adantl
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ y z )
22 7 21 nfeld
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y x e. z )
23 14 22 nfald
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w x e. z )
24 19 23 nfimd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( E. z x e. w -> A. w x e. z ) )
25 13 24 nfald
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. x ( E. z x e. w -> A. w x e. z ) )
26 8 7 nfeld
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y w e. x )
27 25 26 nfimd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
28 14 27 nfald
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
29 13 28 nfexd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) )
30 10 29 nfimd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ y ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) )
31 equequ2
 |-  ( w = y -> ( x = w <-> x = y ) )
32 31 notbid
 |-  ( w = y -> ( -. x = w <-> -. x = y ) )
33 32 adantl
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( -. x = w <-> -. x = y ) )
34 nfcvd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x w )
35 nfcvf2
 |-  ( -. A. y y = x -> F/_ x y )
36 35 adantr
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ x y )
37 34 36 nfeqd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ x w = y )
38 13 37 nfan1
 |-  F/ x ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
39 nfcvd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z w )
40 nfcvf2
 |-  ( -. A. y y = z -> F/_ z y )
41 40 adantl
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/_ z y )
42 39 41 nfeqd
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> F/ z w = y )
43 17 42 nfan1
 |-  F/ z ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y )
44 elequ2
 |-  ( w = y -> ( x e. w <-> x e. y ) )
45 44 adantl
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( x e. w <-> x e. y ) )
46 43 45 exbid
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. z x e. w <-> E. z x e. y ) )
47 biidd
 |-  ( w = y -> ( x e. z <-> x e. z ) )
48 47 a1i
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( x e. z <-> x e. z ) ) )
49 5 22 48 cbvald
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w x e. z <-> A. y x e. z ) )
50 49 adantr
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( A. w x e. z <-> A. y x e. z ) )
51 46 50 imbi12d
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( E. z x e. w -> A. w x e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) )
52 38 51 albid
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( A. x ( E. z x e. w -> A. w x e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
53 elequ1
 |-  ( w = y -> ( w e. x <-> y e. x ) )
54 53 adantl
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( w e. x <-> y e. x ) )
55 52 54 imbi12d
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
56 55 ex
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
57 5 27 56 cbvald
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
58 13 57 exbid
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
59 58 adantr
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
60 33 59 imbi12d
 |-  ( ( ( -. A. y y = x /\ -. A. y y = z ) /\ w = y ) -> ( ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
61 60 ex
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( w = y -> ( ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) ) )
62 5 30 61 cbvald
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( A. w ( -. x = w -> E. x A. w ( A. x ( E. z x e. w -> A. w x e. z ) -> w e. x ) ) <-> A. y ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
63 2 62 mpbii
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> A. y ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
64 63 19.21bi
 |-  ( ( -. A. y y = x /\ -. A. y y = z ) -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
65 64 ex
 |-  ( -. A. y y = x -> ( -. A. y y = z -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )