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∃zx∈y→∀yx∈z→y∈x

Proof

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