Metamath Proof Explorer

Theorem axpowg2

Description: A generalization of ax-pow in which x and w need not be distinct. This theorem scheme bundles ax-pow with the degenerate instance E. y A. z ( A. x ( x e. z -> x e. x ) -> z e. y ) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 ). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 26-May-2026) (New usage is discouraged.)

Ref Expression
Assertion axpowg2 ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ y ¬ ∀ x x = w
2 nfv ⊢ Ⅎ z ¬ ∀ x x = w
3 nfnae ⊢ Ⅎ w ¬ ∀ x x = w
4 nfcvf ⊢ ¬ ∀ x x = w → Ⅎ _ x w
5 nfcvd ⊢ ¬ ∀ x x = w → Ⅎ _ x z
6 4 5 nfeld ⊢ ¬ ∀ x x = w → Ⅎ x w ∈ z
7 nfcvd ⊢ ¬ ∀ x x = w → Ⅎ _ x v
8 4 7 nfeld ⊢ ¬ ∀ x x = w → Ⅎ x w ∈ v
9 6 8 nfimd ⊢ ¬ ∀ x x = w → Ⅎ x w ∈ z → w ∈ v
10 3 9 nfald ⊢ ¬ ∀ x x = w → Ⅎ x ∀ w w ∈ z → w ∈ v
11 nfvd ⊢ ¬ ∀ x x = w → Ⅎ x z ∈ y
12 10 11 nfimd ⊢ ¬ ∀ x x = w → Ⅎ x ∀ w w ∈ z → w ∈ v → z ∈ y
13 2 12 nfald ⊢ ¬ ∀ x x = w → Ⅎ x ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
14 1 13 nfexd ⊢ ¬ ∀ x x = w → Ⅎ x ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
15 nfvd ⊢ ¬ ∀ x x = w → Ⅎ v ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
16 dveeq2 ⊢ ¬ ∀ w w = x → v = x → ∀ w v = x
17 16 naecoms ⊢ ¬ ∀ x x = w → v = x → ∀ w v = x
18 ax9v2 ⊢ x = v → w ∈ x → w ∈ v
19 18 equcoms ⊢ v = x → w ∈ x → w ∈ v
20 19 imim2d ⊢ v = x → w ∈ z → w ∈ x → w ∈ z → w ∈ v
21 20 al2imi ⊢ ∀ w v = x → ∀ w w ∈ z → w ∈ x → ∀ w w ∈ z → w ∈ v
22 21 imim1d ⊢ ∀ w v = x → ∀ w w ∈ z → w ∈ v → z ∈ y → ∀ w w ∈ z → w ∈ x → z ∈ y
23 22 alimdv ⊢ ∀ w v = x → ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y → ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
24 23 eximdv ⊢ ∀ w v = x → ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
25 17 24 syl6 ⊢ ¬ ∀ x x = w → v = x → ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
26 axc11r ⊢ ∀ x x = w → ∀ w w ∈ z → w ∈ x → ∀ x w ∈ z → w ∈ x
27 ax8 ⊢ x = w → x ∈ z → w ∈ z
28 ax8 ⊢ w = x → w ∈ x → x ∈ x
29 28 equcoms ⊢ x = w → w ∈ x → x ∈ x
30 27 29 imim12d ⊢ x = w → w ∈ z → w ∈ x → x ∈ z → x ∈ x
31 30 al2imi ⊢ ∀ x x = w → ∀ x w ∈ z → w ∈ x → ∀ x x ∈ z → x ∈ x
32 26 31 syld ⊢ ∀ x x = w → ∀ w w ∈ z → w ∈ x → ∀ x x ∈ z → x ∈ x
33 32 imim1d ⊢ ∀ x x = w → ∀ x x ∈ z → x ∈ x → z ∈ y → ∀ w w ∈ z → w ∈ x → z ∈ y
34 33 alimdv ⊢ ∀ x x = w → ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y → ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
35 34 eximdv ⊢ ∀ x x = w → ∃ y ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
36 ax-pow ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
37 36 ax-gen ⊢ ∀ v ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
38 axprlem1 ⊢ ∃ y ∀ z ∀ x ¬ x ∈ z → z ∈ y
39 elirrv ⊢ ¬ x ∈ x
40 mtt ⊢ ¬ x ∈ x → ¬ x ∈ z ↔ x ∈ z → x ∈ x
41 39 40 ax-mp ⊢ ¬ x ∈ z ↔ x ∈ z → x ∈ x
42 41 biimpri ⊢ x ∈ z → x ∈ x → ¬ x ∈ z
43 42 alimi ⊢ ∀ x x ∈ z → x ∈ x → ∀ x ¬ x ∈ z
44 43 imim1i ⊢ ∀ x ¬ x ∈ z → z ∈ y → ∀ x x ∈ z → x ∈ x → z ∈ y
45 44 alimi ⊢ ∀ z ∀ x ¬ x ∈ z → z ∈ y → ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y
46 38 45 eximii ⊢ ∃ y ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y
47 46 ax-gen ⊢ ∀ x ∃ y ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y
48 14 15 25 35 37 47 dvelimalcasei ⊢ ∀ x ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
49 48 spi ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y