Theorem pwex 5342

Description: Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
pwex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
pwex	⊢ 𝒫 𝐴 ∈ V

Proof of Theorem pwex

Step	Hyp	Ref	Expression
1		pwex.1	. 2 ⊢ 𝐴 ∈ V
2		pwexg 5340	. 2 ⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-pw 4560

This theorem is referenced by:  p0ex  5346  pp0ex  5348  ord3ex  5349  abexssex  7955  mptmpoopabbrd  8066  fnpm  8819  canth2  9106  dffi3  9379  r1sucg  9729  r1pwALT  9806  rankuni  9823  rankc2  9831  rankxpu  9836  rankmapu  9838  rankxplim  9839  r0weon  9984  aceq3lem  10092  dfac5lem4  10098  dfac2a  10101  dfac2b  10102  pwdju1  10162  ackbij2lem2  10210  ackbij2lem3  10211  fin23lem17  10310  domtriomlem  10414  axdc2lem  10420  axdc3lem  10422  axdclem2  10492  alephsucpw  10543  canthp1lem1  10625  gchac  10654  gruina  10791  npex  10959  nrex1  11037  pnfex  11250  mnfxr  11254  ixxex  13374  prdsvallem  17497  prdsds  17507  prdshom  17510  ismre  17632  fnmre  17633  fnmrc  17653  mrcfval  17654  mrisval  17676  wunfunc  17948  catcfuccl  18165  catcxpccl  18253  lubfval  18394  glbfval  18407  issubmgm  18750  issubm  18851  issubg  19183  cntzfval  19381  sylow1lem2  19660  lsmfval  19699  pj1fval  19755  issubrng  20623  issubrg  20647  rgspnval  20688  lssset  21023  lspfval  21063  islbs  21166  lbsext  21256  lbsexg  21257  sraval  21265  ocvfval  21776  cssval  21792  isobs  21830  islinds  21919  aspval  21982  istopon  23030  dmtopon  23041  fncld  23140  leordtval2  23330  cnpfval  23352  iscnp2  23357  kgenf  23659  xkoopn  23707  xkouni  23717  dfac14  23736  xkoccn  23737  prdstopn  23746  xkoco1cn  23775  xkoco2cn  23776  xkococn  23778  xkoinjcn  23805  isfbas  23947  uzrest  24015  acufl  24035  alexsubALTlem2  24166  tsmsval2  24248  ustfn  24320  ustn0  24339  ishtpy  25092  vitali  25733  madefi  28064  sspval  30984  shex  31473  hsupval  31595  fpwrelmap  32990  fpwrelmapffs  32991  dmvlsiga  34436  eulerpartlem1  34674  eulerpartgbij  34679  eulerpartlemmf  34682  coinflippv  34791  ballotlemoex  34793  reprval  34914  kur14lem9  35577  satfvsuclem1  35722  mpstval  35898  mclsrcl  35924  mclsval  35926  heibor1lem  38320  heibor  38332  idlval  38524  psubspset  40380  paddfval  40433  pclfvalN  40525  polfvalN  40540  psubclsetN  40572  docafvalN  41758  djafvalN  41770  dicval  41812  dochfval  41986  djhfval  42033  islpolN  42119  mzpclval  43318  eldiophb  43350  rpnnen3  43621  dfac11  43651  clsk1independent  44634  permaxpow  45583  dmvolsal  46918  ovnval  47113  smfresal  47360  sprbisymrel  48103  grtri  48560  uspgrex  48770  uspgrbisymrelALT  48775  lincop  49039  setrec2fun  50321  elpglem3  50342