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

Theorem vpwex 5275
 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 5276 from vpwex 5275. (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 4544 . 2 𝒫 𝑥 = {𝑦𝑦𝑥}
2 axpow2 5265 . . . . 5 𝑧𝑦(𝑦𝑥𝑦𝑧)
32bm1.3ii 5203 . . . 4 𝑧𝑦(𝑦𝑧𝑦𝑥)
4 abeq2 2950 . . . . 5 (𝑧 = {𝑦𝑦𝑥} ↔ ∀𝑦(𝑦𝑧𝑦𝑥))
54exbii 1841 . . . 4 (∃𝑧 𝑧 = {𝑦𝑦𝑥} ↔ ∃𝑧𝑦(𝑦𝑧𝑦𝑥))
63, 5mpbir 232 . . 3 𝑧 𝑧 = {𝑦𝑦𝑥}
76issetri 3516 . 2 {𝑦𝑦𝑥} ∈ V
81, 7eqeltri 2914 1 𝒫 𝑥 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207  ∀wal 1528   = wceq 1530  ∃wex 1773   ∈ wcel 2107  {cab 2804  Vcvv 3500   ⊆ wss 3940  𝒫 cpw 4542 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-pow 5263 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-v 3502  df-in 3947  df-ss 3956  df-pw 4544 This theorem is referenced by:  pwexg  5276  pwnex  7470  inf3lem7  9086  dfac8  9550  dfac13  9557  ackbij1lem8  9638  dominf  9856  numthcor  9905  dominfac  9984  intwun  10146  wunex2  10149  eltsk2g  10162  inttsk  10185  tskcard  10192  intgru  10225  gruina  10229  axgroth6  10239  ismre  16851  fnmre  16852  mreacs  16919  isacs5lem  17769  pmtrfval  18498  istopon  21436  dmtopon  21447  tgdom  21502  isfbas  22353  bj-snglex  34169  exrecfnpw  34531  pwinfi  39788  ntrrn  40337  ntrf  40338  dssmapntrcls  40343
 Copyright terms: Public domain W3C validator