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∀ww∈z→w∈x→z∈y

Proof

Step Hyp Ref Expression
1 dtru ⊢¬∀yy=z
2 exnal ⊢∃y¬y=z↔¬∀yy=z
3 1 2 mpbir ⊢∃y¬y=z
4 nfe1 ⊢Ⅎy∃y∀z∀y∃xy∈z→∀zy∈x→z∈y
5 axpownd ⊢¬y=z→∃y∀z∀y∃xy∈z→∀zy∈x→z∈y
6 4 5 exlimi ⊢∃y¬y=z→∃y∀z∀y∃xy∈z→∀zy∈x→z∈y
7 3 6 ax-mp ⊢∃y∀z∀y∃xy∈z→∀zy∈x→z∈y
8 19.9v ⊢∃xy∈z↔y∈z
9 19.3v ⊢∀zy∈x↔y∈x
10 8 9 imbi12i ⊢∃xy∈z→∀zy∈x↔y∈z→y∈x
11 10 albii ⊢∀y∃xy∈z→∀zy∈x↔∀yy∈z→y∈x
12 11 imbi1i ⊢∀y∃xy∈z→∀zy∈x→z∈y↔∀yy∈z→y∈x→z∈y
13 12 albii ⊢∀z∀y∃xy∈z→∀zy∈x→z∈y↔∀z∀yy∈z→y∈x→z∈y
14 13 exbii ⊢∃y∀z∀y∃xy∈z→∀zy∈x→z∈y↔∃y∀z∀yy∈z→y∈x→z∈y
15 7 14 mpbi ⊢∃y∀z∀yy∈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 ⊢∀ww∈z→w∈x↔∀yy∈z→y∈x
20 19 imbi1i ⊢∀ww∈z→w∈x→z∈y↔∀yy∈z→y∈x→z∈y
21 20 albii ⊢∀z∀ww∈z→w∈x→z∈y↔∀z∀yy∈z→y∈x→z∈y
22 21 exbii ⊢∃y∀z∀ww∈z→w∈x→z∈y↔∃y∀z∀yy∈z→y∈x→z∈y
23 15 22 mpbir ⊢∃y∀z∀ww∈z→w∈x→z∈y