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

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