Theorem pwex 5298

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 5296	. 2 ⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  p0ex  5302  pp0ex  5304  ord3ex  5305  abexssex  7786  fnpm  8581  canth2  8866  dffi3  9120  r1sucg  9458  r1pwALT  9535  rankuni  9552  rankc2  9560  rankxpu  9565  rankmapu  9567  rankxplim  9568  r0weon  9699  aceq3lem  9807  dfac5lem4  9813  dfac2a  9816  dfac2b  9817  pwdju1  9877  ackbij2lem2  9927  ackbij2lem3  9928  fin23lem17  10025  domtriomlem  10129  axdc2lem  10135  axdc3lem  10137  axdclem2  10207  alephsucpw  10257  canthp1lem1  10339  gchac  10368  gruina  10505  npex  10673  nrex1  10751  pnfex  10959  mnfxr  10963  ixxex  13019  prdsvallem  17082  prdsds  17092  prdshom  17095  ismre  17216  fnmre  17217  fnmrc  17233  mrcfval  17234  mrisval  17256  wunfunc  17530  wunfuncOLD  17531  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  lubfval  17983  glbfval  17996  issubm  18357  issubg  18670  cntzfval  18841  sylow1lem2  19119  lsmfval  19158  pj1fval  19215  issubrg  19939  lssset  20110  lspfval  20150  islbs  20253  lbsext  20340  lbsexg  20341  sraval  20353  ocvfval  20783  cssval  20799  isobs  20837  islinds  20926  aspval  20987  istopon  21969  dmtopon  21980  fncld  22081  leordtval2  22271  cnpfval  22293  iscnp2  22298  kgenf  22600  xkoopn  22648  xkouni  22658  dfac14  22677  xkoccn  22678  prdstopn  22687  xkoco1cn  22716  xkoco2cn  22717  xkococn  22719  xkoinjcn  22746  isfbas  22888  uzrest  22956  acufl  22976  alexsubALTlem2  23107  tsmsval2  23189  ustfn  23261  ustn0  23280  ishtpy  24041  vitali  24682  sspval  28986  shex  29475  hsupval  29597  fpwrelmap  30970  fpwrelmapffs  30971  dmvlsiga  31997  eulerpartlem1  32234  eulerpartgbij  32239  eulerpartlemmf  32242  coinflippv  32350  ballotlemoex  32352  reprval  32490  kur14lem9  33076  satfvsuclem1  33221  mpstval  33397  mclsrcl  33423  mclsval  33425  heibor1lem  35894  heibor  35906  idlval  36098  psubspset  37685  paddfval  37738  pclfvalN  37830  polfvalN  37845  psubclsetN  37877  docafvalN  39063  djafvalN  39075  dicval  39117  dochfval  39291  djhfval  39338  islpolN  39424  mzpclval  40463  eldiophb  40495  rpnnen3  40770  dfac11  40803  rgspnval  40909  clsk1independent  41545  dmvolsal  43775  ovnval  43969  smfresal  44209  sprbisymrel  44839  uspgrex  45200  uspgrbisymrelALT  45205  issubmgm  45231  lincop  45637  setrec2fun  46284  vsetrec  46294  elpglem3  46304