Theorem vpwex 4775

Description: The powerset of a setvar is a set. (Contributed by BJ, 3-May-2021.)

Assertion

Ref	Expression
vpwex	⊢ 𝒫 𝑥 ∈ V

Proof of Theorem vpwex

Step	Hyp	Ref	Expression
1		vex 3176	. 2 ⊢ 𝑥 ∈ V
2	1	pwex 4774	1 ⊢ 𝒫 𝑥 ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-pow 4769

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  pwexg  4776  inf3lem7  8414  dfac8  8840  dfac13  8847  ackbij1lem5  8929  ackbij1lem8  8932  dominf  9150  numthcor  9199  dominfac  9274  intwun  9436  wunex2  9439  eltsk2g  9452  inttsk  9475  tskcard  9482  intgru  9515  gruina  9519  axgroth6  9529  ismre  16073  fnmre  16074  mreacs  16142  isacs5lem  16992  pmtrfval  17693  istopon  20540  tgdom  20593  isfbas  21443  bj-snglex  32154  bj-dmtopon  32242  bj-pwnex  32246  pwinfi  36888  ntrrn  37440  ntrf  37441  dssmapntrcls  37446