Theorem pwex 5316

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-pw 4538

This theorem is referenced by:  p0ex  5320  pp0ex  5322  ord3ex  5323  abexssex  7919  mptmpoopabbrd  8029  fnpm  8778  canth2  9065  dffi3  9341  r1sucg  9691  r1pwALT  9768  rankuni  9785  rankc2  9793  rankxpu  9798  rankmapu  9800  rankxplim  9801  r0weon  9932  aceq3lem  10040  dfac5lem4  10046  dfac5lem4OLD  10048  dfac2a  10050  dfac2b  10051  pwdju1  10111  ackbij2lem2  10159  ackbij2lem3  10160  fin23lem17  10258  domtriomlem  10362  axdc2lem  10368  axdc3lem  10370  axdclem2  10440  alephsucpw  10491  canthp1lem1  10573  gchac  10602  gruina  10739  npex  10907  nrex1  10985  pnfex  11196  mnfxr  11200  ixxex  13307  prdsvallem  17415  prdsds  17425  prdshom  17428  ismre  17550  fnmre  17551  fnmrc  17571  mrcfval  17572  mrisval  17594  wunfunc  17866  catcfuccl  18083  catcxpccl  18171  lubfval  18312  glbfval  18325  issubmgm  18668  issubm  18769  issubg  19100  cntzfval  19293  sylow1lem2  19572  lsmfval  19611  pj1fval  19667  issubrng  20526  issubrg  20550  rgspnval  20591  lssset  20930  lspfval  20970  islbs  21073  lbsext  21163  lbsexg  21164  sraval  21172  ocvfval  21648  cssval  21664  isobs  21702  islinds  21791  aspval  21854  istopon  22902  dmtopon  22913  fncld  23012  leordtval2  23202  cnpfval  23224  iscnp2  23229  kgenf  23531  xkoopn  23579  xkouni  23589  dfac14  23608  xkoccn  23609  prdstopn  23618  xkoco1cn  23647  xkoco2cn  23648  xkococn  23650  xkoinjcn  23677  isfbas  23819  uzrest  23887  acufl  23907  alexsubALTlem2  24038  tsmsval2  24120  ustfn  24192  ustn0  24211  ishtpy  24964  vitali  25605  madefi  27930  sspval  30819  shex  31308  hsupval  31430  fpwrelmap  32832  fpwrelmapffs  32833  dmvlsiga  34320  eulerpartlem1  34558  eulerpartgbij  34563  eulerpartlemmf  34566  coinflippv  34675  ballotlemoex  34677  reprval  34801  kur14lem9  35449  satfvsuclem1  35594  mpstval  35770  mclsrcl  35796  mclsval  35798  heibor1lem  38183  heibor  38195  idlval  38387  psubspset  40243  paddfval  40296  pclfvalN  40388  polfvalN  40403  psubclsetN  40435  docafvalN  41621  djafvalN  41633  dicval  41675  dochfval  41849  djhfval  41896  islpolN  41982  mzpclval  43181  eldiophb  43213  rpnnen3  43484  dfac11  43514  clsk1independent  44497  permaxpow  45460  dmvolsal  46796  ovnval  46991  smfresal  47238  sprbisymrel  47981  grtri  48438  uspgrex  48648  uspgrbisymrelALT  48653  lincop  48906  setrec2fun  50189  elpglem3  50210