Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axpweq Structured version   Visualization version   GIF version

Theorem axpweq 5237
 Description: Two equivalent ways to express the Power Set Axiom. Note that ax-pow 5238 is not used by the proof. When ax-pow 5238 is assumed and 𝐴 is a set, both sides of the biconditional hold. In ZF, both sides hold if and only if 𝐴 is a set (see pwexr 7492). (Contributed by NM, 22-Jun-2009.)
Assertion
Ref Expression
axpweq (𝒫 𝐴 ∈ V ↔ ∃𝑥𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑧,𝐴,𝑦

Proof of Theorem axpweq
StepHypRef Expression
1 pwidg 4519 . . . 4 (𝒫 𝐴 ∈ V → 𝒫 𝐴 ∈ 𝒫 𝒫 𝐴)
2 pweq 4513 . . . . . 6 (𝑥 = 𝒫 𝐴 → 𝒫 𝑥 = 𝒫 𝒫 𝐴)
32eleq2d 2837 . . . . 5 (𝑥 = 𝒫 𝐴 → (𝒫 𝐴 ∈ 𝒫 𝑥 ↔ 𝒫 𝐴 ∈ 𝒫 𝒫 𝐴))
43spcegv 3517 . . . 4 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ 𝒫 𝒫 𝐴 → ∃𝑥𝒫 𝐴 ∈ 𝒫 𝑥))
51, 4mpd 15 . . 3 (𝒫 𝐴 ∈ V → ∃𝑥𝒫 𝐴 ∈ 𝒫 𝑥)
6 elex 3428 . . . 4 (𝒫 𝐴 ∈ 𝒫 𝑥 → 𝒫 𝐴 ∈ V)
76exlimiv 1931 . . 3 (∃𝑥𝒫 𝐴 ∈ 𝒫 𝑥 → 𝒫 𝐴 ∈ V)
85, 7impbii 212 . 2 (𝒫 𝐴 ∈ V ↔ ∃𝑥𝒫 𝐴 ∈ 𝒫 𝑥)
9 vex 3413 . . . . 5 𝑥 ∈ V
109elpw2 5219 . . . 4 (𝒫 𝐴 ∈ 𝒫 𝑥 ↔ 𝒫 𝐴𝑥)
11 pwss 4522 . . . . 5 (𝒫 𝐴𝑥 ↔ ∀𝑦(𝑦𝐴𝑦𝑥))
12 dfss2 3880 . . . . . . 7 (𝑦𝐴 ↔ ∀𝑧(𝑧𝑦𝑧𝐴))
1312imbi1i 353 . . . . . 6 ((𝑦𝐴𝑦𝑥) ↔ (∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
1413albii 1821 . . . . 5 (∀𝑦(𝑦𝐴𝑦𝑥) ↔ ∀𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
1511, 14bitri 278 . . . 4 (𝒫 𝐴𝑥 ↔ ∀𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
1610, 15bitri 278 . . 3 (𝒫 𝐴 ∈ 𝒫 𝑥 ↔ ∀𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
1716exbii 1849 . 2 (∃𝑥𝒫 𝐴 ∈ 𝒫 𝑥 ↔ ∃𝑥𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
188, 17bitri 278 1 (𝒫 𝐴 ∈ V ↔ ∃𝑥𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3409   ⊆ wss 3860  𝒫 cpw 4497 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5173 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-in 3867  df-ss 3877  df-pw 4499 This theorem is referenced by:  grothpw  10299
 Copyright terms: Public domain W3C validator