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

Theorem vpwex 4998
Description: The powerset of a setvar is a set. (Contributed by BJ, 3-May-2021.)
Assertion
Ref Expression
vpwex 𝒫 𝑥 ∈ V

Proof of Theorem vpwex
StepHypRef Expression
1 vex 3343 . 2 𝑥 ∈ V
21pwex 4997 1 𝒫 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  Vcvv 3340  𝒫 cpw 4302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-pow 4992
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-v 3342  df-in 3722  df-ss 3729  df-pw 4304
This theorem is referenced by:  pwexg  4999  pwnex  7133  inf3lem7  8704  dfac8  9149  dfac13  9156  ackbij1lem5  9238  ackbij1lem8  9241  dominf  9459  numthcor  9508  dominfac  9587  intwun  9749  wunex2  9752  eltsk2g  9765  inttsk  9788  tskcard  9795  intgru  9828  gruina  9832  axgroth6  9842  ismre  16452  fnmre  16453  mreacs  16520  isacs5lem  17370  pmtrfval  18070  istopon  20919  dmtopon  20929  tgdom  20984  isfbas  21834  bj-snglex  33267  pwinfi  38371  ntrrn  38922  ntrf  38923  dssmapntrcls  38928
  Copyright terms: Public domain W3C validator