Theorem pwex 5318

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  𝒫 cpw 4550

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 5234  ax-pow 5303

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 3919  df-pw 4552

This theorem is referenced by:  p0ex  5322  pp0ex  5324  ord3ex  5325  abexssex  7902  mptmpoopabbrd  8012  fnpm  8758  canth2  9043  dffi3  9315  r1sucg  9659  r1pwALT  9736  rankuni  9753  rankc2  9761  rankxpu  9766  rankmapu  9768  rankxplim  9769  r0weon  9900  aceq3lem  10008  dfac5lem4  10014  dfac5lem4OLD  10016  dfac2a  10018  dfac2b  10019  pwdju1  10079  ackbij2lem2  10127  ackbij2lem3  10128  fin23lem17  10226  domtriomlem  10330  axdc2lem  10336  axdc3lem  10338  axdclem2  10408  alephsucpw  10458  canthp1lem1  10540  gchac  10569  gruina  10706  npex  10874  nrex1  10952  pnfex  11162  mnfxr  11166  ixxex  13253  prdsvallem  17355  prdsds  17365  prdshom  17368  ismre  17489  fnmre  17490  fnmrc  17510  mrcfval  17511  mrisval  17533  wunfunc  17805  catcfuccl  18022  catcxpccl  18110  lubfval  18251  glbfval  18264  issubmgm  18607  issubm  18708  issubg  19036  cntzfval  19230  sylow1lem2  19509  lsmfval  19548  pj1fval  19604  issubrng  20460  issubrg  20484  rgspnval  20525  lssset  20864  lspfval  20904  islbs  21008  lbsext  21098  lbsexg  21099  sraval  21107  ocvfval  21601  cssval  21617  isobs  21655  islinds  21744  aspval  21808  istopon  22825  dmtopon  22836  fncld  22935  leordtval2  23125  cnpfval  23147  iscnp2  23152  kgenf  23454  xkoopn  23502  xkouni  23512  dfac14  23531  xkoccn  23532  prdstopn  23541  xkoco1cn  23570  xkoco2cn  23571  xkococn  23573  xkoinjcn  23600  isfbas  23742  uzrest  23810  acufl  23830  alexsubALTlem2  23961  tsmsval2  24043  ustfn  24115  ustn0  24134  ishtpy  24896  vitali  25539  madefi  27856  sspval  30698  shex  31187  hsupval  31309  fpwrelmap  32711  fpwrelmapffs  32712  dmvlsiga  34137  eulerpartlem1  34375  eulerpartgbij  34380  eulerpartlemmf  34383  coinflippv  34492  ballotlemoex  34494  reprval  34618  kur14lem9  35246  satfvsuclem1  35391  mpstval  35567  mclsrcl  35593  mclsval  35595  heibor1lem  37848  heibor  37860  idlval  38052  psubspset  39782  paddfval  39835  pclfvalN  39927  polfvalN  39942  psubclsetN  39974  docafvalN  41160  djafvalN  41172  dicval  41214  dochfval  41388  djhfval  41435  islpolN  41521  mzpclval  42757  eldiophb  42789  rpnnen3  43064  dfac11  43094  clsk1independent  44078  permaxpow  45041  dmvolsal  46383  ovnval  46578  smfresal  46825  sprbisymrel  47529  grtri  47970  uspgrex  48180  uspgrbisymrelALT  48185  lincop  48439  setrec2fun  49723  elpglem3  49744