Theorem pwex 5327

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  p0ex  5331  pp0ex  5333  ord3ex  5334  abexssex  7924  mptmpoopabbrd  8034  fnpm  8783  canth2  9070  dffi3  9346  r1sucg  9693  r1pwALT  9770  rankuni  9787  rankc2  9795  rankxpu  9800  rankmapu  9802  rankxplim  9803  r0weon  9934  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2a  10052  dfac2b  10053  pwdju1  10113  ackbij2lem2  10161  ackbij2lem3  10162  fin23lem17  10260  domtriomlem  10364  axdc2lem  10370  axdc3lem  10372  axdclem2  10442  alephsucpw  10493  canthp1lem1  10575  gchac  10604  gruina  10741  npex  10909  nrex1  10987  pnfex  11197  mnfxr  11201  ixxex  13284  prdsvallem  17386  prdsds  17396  prdshom  17399  ismre  17521  fnmre  17522  fnmrc  17542  mrcfval  17543  mrisval  17565  wunfunc  17837  catcfuccl  18054  catcxpccl  18142  lubfval  18283  glbfval  18296  issubmgm  18639  issubm  18740  issubg  19068  cntzfval  19261  sylow1lem2  19540  lsmfval  19579  pj1fval  19635  issubrng  20492  issubrg  20516  rgspnval  20557  lssset  20896  lspfval  20936  islbs  21040  lbsext  21130  lbsexg  21131  sraval  21139  ocvfval  21633  cssval  21649  isobs  21687  islinds  21776  aspval  21840  istopon  22868  dmtopon  22879  fncld  22978  leordtval2  23168  cnpfval  23190  iscnp2  23195  kgenf  23497  xkoopn  23545  xkouni  23555  dfac14  23574  xkoccn  23575  prdstopn  23584  xkoco1cn  23613  xkoco2cn  23614  xkococn  23616  xkoinjcn  23643  isfbas  23785  uzrest  23853  acufl  23873  alexsubALTlem2  24004  tsmsval2  24086  ustfn  24158  ustn0  24177  ishtpy  24939  vitali  25582  madefi  27921  sspval  30810  shex  31299  hsupval  31421  fpwrelmap  32822  fpwrelmapffs  32823  dmvlsiga  34306  eulerpartlem1  34544  eulerpartgbij  34549  eulerpartlemmf  34552  coinflippv  34661  ballotlemoex  34663  reprval  34787  kur14lem9  35427  satfvsuclem1  35572  mpstval  35748  mclsrcl  35774  mclsval  35776  heibor1lem  38054  heibor  38066  idlval  38258  psubspset  40114  paddfval  40167  pclfvalN  40259  polfvalN  40274  psubclsetN  40306  docafvalN  41492  djafvalN  41504  dicval  41546  dochfval  41720  djhfval  41767  islpolN  41853  mzpclval  43076  eldiophb  43108  rpnnen3  43383  dfac11  43413  clsk1independent  44396  permaxpow  45359  dmvolsal  46698  ovnval  46893  smfresal  47140  sprbisymrel  47853  grtri  48294  uspgrex  48504  uspgrbisymrelALT  48509  lincop  48762  setrec2fun  50045  elpglem3  50066