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

Theorem vpwex 5300
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 5301 from vpwex 5300. (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 4535 . 2 𝒫 𝑥 = {𝑤𝑤𝑥}
2 axpow2 5290 . . . . 5 𝑦𝑧(𝑧𝑥𝑧𝑦)
32bm1.3ii 5226 . . . 4 𝑦𝑧(𝑧𝑦𝑧𝑥)
4 sseq1 3946 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝑥𝑧𝑥))
54abeq2w 2815 . . . . 5 (𝑦 = {𝑤𝑤𝑥} ↔ ∀𝑧(𝑧𝑦𝑧𝑥))
65exbii 1850 . . . 4 (∃𝑦 𝑦 = {𝑤𝑤𝑥} ↔ ∃𝑦𝑧(𝑧𝑦𝑧𝑥))
73, 6mpbir 230 . . 3 𝑦 𝑦 = {𝑤𝑤𝑥}
87issetri 3448 . 2 {𝑤𝑤𝑥} ∈ V
91, 8eqeltri 2835 1 𝒫 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wb 205  wal 1537   = wceq 1539  wex 1782  wcel 2106  {cab 2715  Vcvv 3432  wss 3887  𝒫 cpw 4533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-pow 5288
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535
This theorem is referenced by:  pwexg  5301  pwnex  7609  inf3lem7  9392  dfac8  9891  dfac13  9898  ackbij1lem8  9983  dominf  10201  numthcor  10250  dominfac  10329  intwun  10491  wunex2  10494  eltsk2g  10507  inttsk  10530  tskcard  10537  intgru  10570  gruina  10574  axgroth6  10584  ismre  17299  fnmre  17300  mreacs  17367  isacs5lem  18263  pmtrfval  19058  istopon  22061  dmtopon  22072  tgdom  22128  isfbas  22980  bj-snglex  35163  exrecfnpw  35552  pwinfi  41171  ntrrn  41732  ntrf  41733  dssmapntrcls  41738
  Copyright terms: Public domain W3C validator