Theorem pwex 5336

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-pw 4556

This theorem is referenced by:  p0ex  5340  pp0ex  5342  ord3ex  5343  abexssex  7947  mptmpoopabbrd  8057  fnpm  8811  canth2  9098  dffi3  9374  r1sucg  9724  r1pwALT  9801  rankuni  9818  rankc2  9826  rankxpu  9831  rankmapu  9833  rankxplim  9834  r0weon  9965  aceq3lem  10073  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2a  10083  dfac2b  10084  pwdju1  10144  ackbij2lem2  10192  ackbij2lem3  10193  fin23lem17  10292  domtriomlem  10396  axdc2lem  10402  axdc3lem  10404  axdclem2  10474  alephsucpw  10525  canthp1lem1  10607  gchac  10636  gruina  10773  npex  10941  nrex1  11019  pnfex  11232  mnfxr  11236  ixxex  13357  prdsvallem  17466  prdsds  17476  prdshom  17479  ismre  17601  fnmre  17602  fnmrc  17622  mrcfval  17623  mrisval  17645  wunfunc  17917  catcfuccl  18134  catcxpccl  18222  lubfval  18363  glbfval  18376  issubmgm  18719  issubm  18820  issubg  19151  cntzfval  19343  sylow1lem2  19622  lsmfval  19661  pj1fval  19717  issubrng  20576  issubrg  20600  rgspnval  20641  lssset  20980  lspfval  21020  islbs  21123  lbsext  21213  lbsexg  21214  sraval  21222  ocvfval  21698  cssval  21714  isobs  21752  islinds  21841  aspval  21904  istopon  22952  dmtopon  22963  fncld  23062  leordtval2  23252  cnpfval  23274  iscnp2  23279  kgenf  23581  xkoopn  23629  xkouni  23639  dfac14  23658  xkoccn  23659  prdstopn  23668  xkoco1cn  23697  xkoco2cn  23698  xkococn  23700  xkoinjcn  23727  isfbas  23869  uzrest  23937  acufl  23957  alexsubALTlem2  24088  tsmsval2  24170  ustfn  24242  ustn0  24261  ishtpy  25014  vitali  25655  madefi  27983  sspval  30872  shex  31361  hsupval  31483  fpwrelmap  32885  fpwrelmapffs  32886  dmvlsiga  34387  eulerpartlem1  34625  eulerpartgbij  34630  eulerpartlemmf  34633  coinflippv  34742  ballotlemoex  34744  reprval  34868  kur14lem9  35528  satfvsuclem1  35673  mpstval  35849  mclsrcl  35875  mclsval  35877  heibor1lem  38272  heibor  38284  idlval  38476  psubspset  40332  paddfval  40385  pclfvalN  40477  polfvalN  40492  psubclsetN  40524  docafvalN  41710  djafvalN  41722  dicval  41764  dochfval  41938  djhfval  41985  islpolN  42071  mzpclval  43270  eldiophb  43302  rpnnen3  43573  dfac11  43603  clsk1independent  44586  permaxpow  45549  dmvolsal  46884  ovnval  47079  smfresal  47326  sprbisymrel  48069  grtri  48526  uspgrex  48736  uspgrbisymrelALT  48741  lincop  48994  setrec2fun  50277  elpglem3  50298