Theorem pwex 5338

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  𝒫 cpw 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-pow 5323

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  p0ex  5342  pp0ex  5344  ord3ex  5345  abexssex  7952  mptmpoopabbrd  8062  fnpm  8810  canth2  9100  dffi3  9389  r1sucg  9729  r1pwALT  9806  rankuni  9823  rankc2  9831  rankxpu  9836  rankmapu  9838  rankxplim  9839  r0weon  9972  aceq3lem  10080  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2a  10090  dfac2b  10091  pwdju1  10151  ackbij2lem2  10199  ackbij2lem3  10200  fin23lem17  10298  domtriomlem  10402  axdc2lem  10408  axdc3lem  10410  axdclem2  10480  alephsucpw  10530  canthp1lem1  10612  gchac  10641  gruina  10778  npex  10946  nrex1  11024  pnfex  11234  mnfxr  11238  ixxex  13324  prdsvallem  17424  prdsds  17434  prdshom  17437  ismre  17558  fnmre  17559  fnmrc  17575  mrcfval  17576  mrisval  17598  wunfunc  17870  catcfuccl  18087  catcxpccl  18175  lubfval  18316  glbfval  18329  issubmgm  18636  issubm  18737  issubg  19065  cntzfval  19259  sylow1lem2  19536  lsmfval  19575  pj1fval  19631  issubrng  20463  issubrg  20487  rgspnval  20528  lssset  20846  lspfval  20886  islbs  20990  lbsext  21080  lbsexg  21081  sraval  21089  ocvfval  21582  cssval  21598  isobs  21636  islinds  21725  aspval  21789  istopon  22806  dmtopon  22817  fncld  22916  leordtval2  23106  cnpfval  23128  iscnp2  23133  kgenf  23435  xkoopn  23483  xkouni  23493  dfac14  23512  xkoccn  23513  prdstopn  23522  xkoco1cn  23551  xkoco2cn  23552  xkococn  23554  xkoinjcn  23581  isfbas  23723  uzrest  23791  acufl  23811  alexsubALTlem2  23942  tsmsval2  24024  ustfn  24096  ustn0  24115  ishtpy  24878  vitali  25521  madefi  27831  sspval  30659  shex  31148  hsupval  31270  fpwrelmap  32663  fpwrelmapffs  32664  dmvlsiga  34126  eulerpartlem1  34365  eulerpartgbij  34370  eulerpartlemmf  34373  coinflippv  34482  ballotlemoex  34484  reprval  34608  kur14lem9  35208  satfvsuclem1  35353  mpstval  35529  mclsrcl  35555  mclsval  35557  heibor1lem  37810  heibor  37822  idlval  38014  psubspset  39745  paddfval  39798  pclfvalN  39890  polfvalN  39905  psubclsetN  39937  docafvalN  41123  djafvalN  41135  dicval  41177  dochfval  41351  djhfval  41398  islpolN  41484  mzpclval  42720  eldiophb  42752  rpnnen3  43028  dfac11  43058  clsk1independent  44042  permaxpow  45006  dmvolsal  46351  ovnval  46546  smfresal  46793  sprbisymrel  47504  grtri  47943  uspgrex  48142  uspgrbisymrelALT  48147  lincop  48401  setrec2fun  49685  elpglem3  49706