Theorem vpwex 4849

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

Assertion

Ref	Expression
vpwex	|- ~P x e. _V

Proof of Theorem vpwex

Step	Hyp	Ref	Expression
1		vex 3203	. 2 |- x e. _V
2	1	pwex 4848	1 |- ~P x e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  pwexg  4850  pwnex  6968  inf3lem7  8531  dfac8  8957  dfac13  8964  ackbij1lem5  9046  ackbij1lem8  9049  dominf  9267  numthcor  9316  dominfac  9395  intwun  9557  wunex2  9560  eltsk2g  9573  inttsk  9596  tskcard  9603  intgru  9636  gruina  9640  axgroth6  9650  ismre  16250  fnmre  16251  mreacs  16319  isacs5lem  17169  pmtrfval  17870  istopon  20717  dmtopon  20727  tgdom  20782  isfbas  21633  bj-snglex  32961  pwinfi  37869  ntrrn  38420  ntrf  38421  dssmapntrcls  38426