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

Theorem vpwex 5383
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 5384 from vpwex 5383. (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 4607 . 2 𝒫 𝑥 = {𝑤𝑤𝑥}
2 axpow2 5373 . . . . 5 𝑦𝑧(𝑧𝑥𝑧𝑦)
32sepexi 5307 . . . 4 𝑦𝑧(𝑧𝑦𝑧𝑥)
4 sseq1 4021 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝑥𝑧𝑥))
54eqabbw 2813 . . . . 5 (𝑦 = {𝑤𝑤𝑥} ↔ ∀𝑧(𝑧𝑦𝑧𝑥))
65exbii 1845 . . . 4 (∃𝑦 𝑦 = {𝑤𝑤𝑥} ↔ ∃𝑦𝑧(𝑧𝑦𝑧𝑥))
73, 6mpbir 231 . . 3 𝑦 𝑦 = {𝑤𝑤𝑥}
87issetri 3497 . 2 {𝑤𝑤𝑥} ∈ V
91, 8eqeltri 2835 1 𝒫 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1535   = wceq 1537  wex 1776  wcel 2106  {cab 2712  Vcvv 3478  wss 3963  𝒫 cpw 4605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-pow 5371
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-pw 4607
This theorem is referenced by:  pwexg  5384  pwnex  7778  inf3lem7  9672  dfac8  10174  dfac13  10181  ackbij1lem8  10264  dominf  10483  numthcor  10532  dominfac  10611  intwun  10773  wunex2  10776  eltsk2g  10789  inttsk  10812  tskcard  10819  intgru  10852  gruina  10856  axgroth6  10866  ismre  17635  fnmre  17636  mreacs  17703  isacs5lem  18603  pmtrfval  19483  istopon  22934  dmtopon  22945  tgdom  23001  isfbas  23853  bj-snglex  36956  exrecfnpw  37364  pwinfi  43554  ntrrn  44112  ntrf  44113  dssmapntrcls  44118  vsetrec  48934  pgindnf  48947
  Copyright terms: Public domain W3C validator