Metamath Proof Explorer

Theorem axpownd

Description: A version of 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) (New usage is discouraged.)

Ref Expression
Assertion axpownd ⊢ ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 axpowndlem4 ⊢ ¬ ∀ y y = x → ¬ ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
2 axpowndlem1 ⊢ ∀ x x = y → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
3 2 aecoms ⊢ ∀ y y = x → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
4 2 a1d ⊢ ∀ x x = y → ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
5 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
6 nfae ⊢ Ⅎ y ∀ y y = z
7 5 6 nfan ⊢ Ⅎ y ¬ ∀ x x = y ∧ ∀ y y = z
8 el ⊢ ∃ w x ∈ w
9 nfcvf2 ⊢ ¬ ∀ x x = y → Ⅎ _ y x
10 nfcvd ⊢ ¬ ∀ x x = y → Ⅎ _ y w
11 9 10 nfeld ⊢ ¬ ∀ x x = y → Ⅎ y x ∈ w
12 elequ2 ⊢ w = y → x ∈ w ↔ x ∈ y
13 12 a1i ⊢ ¬ ∀ x x = y → w = y → x ∈ w ↔ x ∈ y
14 5 11 13 cbvexd ⊢ ¬ ∀ x x = y → ∃ w x ∈ w ↔ ∃ y x ∈ y
15 8 14 mpbii ⊢ ¬ ∀ x x = y → ∃ y x ∈ y
16 15 19.8ad ⊢ ¬ ∀ x x = y → ∃ x ∃ y x ∈ y
17 df-ex ⊢ ∃ x ∃ y x ∈ y ↔ ¬ ∀ x ¬ ∃ y x ∈ y
18 16 17 sylib ⊢ ¬ ∀ x x = y → ¬ ∀ x ¬ ∃ y x ∈ y
19 18 adantr ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ¬ ∀ x ¬ ∃ y x ∈ y
20 biidd ⊢ ∀ y y = z → ¬ x ∈ y ↔ ¬ x ∈ y
21 20 dral1 ⊢ ∀ y y = z → ∀ y ¬ x ∈ y ↔ ∀ z ¬ x ∈ y
22 alnex ⊢ ∀ y ¬ x ∈ y ↔ ¬ ∃ y x ∈ y
23 alnex ⊢ ∀ z ¬ x ∈ y ↔ ¬ ∃ z x ∈ y
24 21 22 23 3bitr3g ⊢ ∀ y y = z → ¬ ∃ y x ∈ y ↔ ¬ ∃ z x ∈ y
25 nd2 ⊢ ∀ y y = z → ¬ ∀ y x ∈ z
26 mtt ⊢ ¬ ∀ y x ∈ z → ¬ ∃ z x ∈ y ↔ ∃ z x ∈ y → ∀ y x ∈ z
27 25 26 syl ⊢ ∀ y y = z → ¬ ∃ z x ∈ y ↔ ∃ z x ∈ y → ∀ y x ∈ z
28 24 27 bitrd ⊢ ∀ y y = z → ¬ ∃ y x ∈ y ↔ ∃ z x ∈ y → ∀ y x ∈ z
29 28 dral2 ⊢ ∀ y y = z → ∀ x ¬ ∃ y x ∈ y ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z
30 29 adantl ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ∀ x ¬ ∃ y x ∈ y ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z
31 19 30 mtbid ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ¬ ∀ x ∃ z x ∈ y → ∀ y x ∈ z
32 31 pm2.21d ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
33 7 32 alrimi ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
34 33 19.8ad ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
35 34 a1d ⊢ ¬ ∀ x x = y ∧ ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
36 35 ex ⊢ ¬ ∀ x x = y → ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
37 4 36 pm2.61i ⊢ ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
38 1 3 37 pm2.61ii ⊢ ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x