Metamath Proof Explorer

Theorem zfcndpow

Description: Axiom of Power Sets ax-pow , reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dtru ⊢ ¬ ∀ y y = z
2 exnal ⊢ ∃ y ¬ y = z ↔ ¬ ∀ y y = z
3 1 2 mpbir ⊢ ∃ y ¬ y = z
4 nfe1 ⊢ Ⅎ y ∃ y ∀ z ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y
5 axpownd ⊢ ¬ y = z → ∃ y ∀ z ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y
6 4 5 exlimi ⊢ ∃ y ¬ y = z → ∃ y ∀ z ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y
7 3 6 ax-mp ⊢ ∃ y ∀ z ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y
8 19.9v ⊢ ∃ x y ∈ z ↔ y ∈ z
9 19.3v ⊢ ∀ z y ∈ x ↔ y ∈ x
10 8 9 imbi12i ⊢ ∃ x y ∈ z → ∀ z y ∈ x ↔ y ∈ z → y ∈ x
11 10 albii ⊢ ∀ y ∃ x y ∈ z → ∀ z y ∈ x ↔ ∀ y y ∈ z → y ∈ x
12 11 imbi1i ⊢ ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y ↔ ∀ y y ∈ z → y ∈ x → z ∈ y
13 12 albii ⊢ ∀ z ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y ↔ ∀ z ∀ y y ∈ z → y ∈ x → z ∈ y
14 13 exbii ⊢ ∃ y ∀ z ∀ y ∃ x y ∈ z → ∀ z y ∈ x → z ∈ y ↔ ∃ y ∀ z ∀ y y ∈ z → y ∈ x → z ∈ y
15 7 14 mpbi ⊢ ∃ y ∀ z ∀ y y ∈ z → y ∈ x → z ∈ y
16 elequ1 ⊢ w = y → w ∈ z ↔ y ∈ z
17 elequ1 ⊢ w = y → w ∈ x ↔ y ∈ x
18 16 17 imbi12d ⊢ w = y → w ∈ z → w ∈ x ↔ y ∈ z → y ∈ x
19 18 cbvalvw ⊢ ∀ w w ∈ z → w ∈ x ↔ ∀ y y ∈ z → y ∈ x
20 19 imbi1i ⊢ ∀ w w ∈ z → w ∈ x → z ∈ y ↔ ∀ y y ∈ z → y ∈ x → z ∈ y
21 20 albii ⊢ ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y ↔ ∀ z ∀ y y ∈ z → y ∈ x → z ∈ y
22 21 exbii ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y ↔ ∃ y ∀ z ∀ y y ∈ z → y ∈ x → z ∈ y
23 15 22 mpbir ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y