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

Theorem vpwex 5377
Description: Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 5378 from vpwex 5377. (Revised by BJ, 10-Aug-2022.)
Assertion
Ref Expression
vpwex 𝒫 𝑥 ∈ V

Proof of Theorem vpwex
Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-pw 4602 . 2 𝒫 𝑥 = {𝑤𝑤𝑥}
2 axpow2 5367 . . . . 5 𝑦𝑧(𝑧𝑥𝑧𝑦)
32sepexi 5301 . . . 4 𝑦𝑧(𝑧𝑦𝑧𝑥)
4 sseq1 4009 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝑥𝑧𝑥))
54eqabbw 2815 . . . . 5 (𝑦 = {𝑤𝑤𝑥} ↔ ∀𝑧(𝑧𝑦𝑧𝑥))
65exbii 1848 . . . 4 (∃𝑦 𝑦 = {𝑤𝑤𝑥} ↔ ∃𝑦𝑧(𝑧𝑦𝑧𝑥))
73, 6mpbir 231 . . 3 𝑦 𝑦 = {𝑤𝑤𝑥}
87issetri 3499 . 2 {𝑤𝑤𝑥} ∈ V
91, 8eqeltri 2837 1 𝒫 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1538   = wceq 1540  wex 1779  wcel 2108  {cab 2714  Vcvv 3480  wss 3951  𝒫 cpw 4600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602
This theorem is referenced by:  pwexg  5378  pwnex  7779  inf3lem7  9674  dfac8  10176  dfac13  10183  ackbij1lem8  10266  dominf  10485  numthcor  10534  dominfac  10613  intwun  10775  wunex2  10778  eltsk2g  10791  inttsk  10814  tskcard  10821  intgru  10854  gruina  10858  axgroth6  10868  ismre  17633  fnmre  17634  mreacs  17701  isacs5lem  18590  pmtrfval  19468  istopon  22918  dmtopon  22929  tgdom  22985  isfbas  23837  bj-snglex  36974  exrecfnpw  37382  pwinfi  43577  ntrrn  44135  ntrf  44136  dssmapntrcls  44141  vsetrec  49222  pgindnf  49235
  Copyright terms: Public domain W3C validator