Theorem pwex 5320

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-pow 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4551

This theorem is referenced by:  p0ex  5324  pp0ex  5326  ord3ex  5327  abexssex  7908  mptmpoopabbrd  8018  fnpm  8764  canth2  9049  dffi3  9321  r1sucg  9668  r1pwALT  9745  rankuni  9762  rankc2  9770  rankxpu  9775  rankmapu  9777  rankxplim  9778  r0weon  9909  aceq3lem  10017  dfac5lem4  10023  dfac5lem4OLD  10025  dfac2a  10027  dfac2b  10028  pwdju1  10088  ackbij2lem2  10136  ackbij2lem3  10137  fin23lem17  10235  domtriomlem  10339  axdc2lem  10345  axdc3lem  10347  axdclem2  10417  alephsucpw  10467  canthp1lem1  10549  gchac  10578  gruina  10715  npex  10883  nrex1  10961  pnfex  11171  mnfxr  11175  ixxex  13262  prdsvallem  17364  prdsds  17374  prdshom  17377  ismre  17498  fnmre  17499  fnmrc  17519  mrcfval  17520  mrisval  17542  wunfunc  17814  catcfuccl  18031  catcxpccl  18119  lubfval  18260  glbfval  18273  issubmgm  18616  issubm  18717  issubg  19045  cntzfval  19238  sylow1lem2  19517  lsmfval  19556  pj1fval  19612  issubrng  20468  issubrg  20492  rgspnval  20533  lssset  20872  lspfval  20912  islbs  21016  lbsext  21106  lbsexg  21107  sraval  21115  ocvfval  21609  cssval  21625  isobs  21663  islinds  21752  aspval  21816  istopon  22833  dmtopon  22844  fncld  22943  leordtval2  23133  cnpfval  23155  iscnp2  23160  kgenf  23462  xkoopn  23510  xkouni  23520  dfac14  23539  xkoccn  23540  prdstopn  23549  xkoco1cn  23578  xkoco2cn  23579  xkococn  23581  xkoinjcn  23608  isfbas  23750  uzrest  23818  acufl  23838  alexsubALTlem2  23969  tsmsval2  24051  ustfn  24123  ustn0  24142  ishtpy  24904  vitali  25547  madefi  27864  sspval  30710  shex  31199  hsupval  31321  fpwrelmap  32723  fpwrelmapffs  32724  dmvlsiga  34149  eulerpartlem1  34387  eulerpartgbij  34392  eulerpartlemmf  34395  coinflippv  34504  ballotlemoex  34506  reprval  34630  kur14lem9  35265  satfvsuclem1  35410  mpstval  35586  mclsrcl  35612  mclsval  35614  heibor1lem  37855  heibor  37867  idlval  38059  psubspset  39849  paddfval  39902  pclfvalN  39994  polfvalN  40009  psubclsetN  40041  docafvalN  41227  djafvalN  41239  dicval  41281  dochfval  41455  djhfval  41502  islpolN  41588  mzpclval  42823  eldiophb  42855  rpnnen3  43130  dfac11  43160  clsk1independent  44144  permaxpow  45107  dmvolsal  46449  ovnval  46644  smfresal  46891  sprbisymrel  47604  grtri  48045  uspgrex  48255  uspgrbisymrelALT  48260  lincop  48514  setrec2fun  49798  elpglem3  49819