Theorem pwex 5322

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  𝒫 cpw 4541

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 2708  ax-sep 5231  ax-pow 5307

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  p0ex  5326  pp0ex  5328  ord3ex  5329  abexssex  7923  mptmpoopabbrd  8033  fnpm  8781  canth2  9068  dffi3  9344  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  11198  mnfxr  11202  ixxex  13309  prdsvallem  17417  prdsds  17427  prdshom  17430  ismre  17552  fnmre  17553  fnmrc  17573  mrcfval  17574  mrisval  17596  wunfunc  17868  catcfuccl  18085  catcxpccl  18173  lubfval  18314  glbfval  18327  issubmgm  18670  issubm  18771  issubg  19102  cntzfval  19295  sylow1lem2  19574  lsmfval  19613  pj1fval  19669  issubrng  20524  issubrg  20548  rgspnval  20589  lssset  20928  lspfval  20968  islbs  21071  lbsext  21161  lbsexg  21162  sraval  21170  ocvfval  21646  cssval  21662  isobs  21700  islinds  21789  aspval  21852  istopon  22877  dmtopon  22888  fncld  22987  leordtval2  23177  cnpfval  23199  iscnp2  23204  kgenf  23506  xkoopn  23554  xkouni  23564  dfac14  23583  xkoccn  23584  prdstopn  23593  xkoco1cn  23622  xkoco2cn  23623  xkococn  23625  xkoinjcn  23652  isfbas  23794  uzrest  23862  acufl  23882  alexsubALTlem2  24013  tsmsval2  24095  ustfn  24167  ustn0  24186  ishtpy  24939  vitali  25580  madefi  27905  sspval  30794  shex  31283  hsupval  31405  fpwrelmap  32806  fpwrelmapffs  32807  dmvlsiga  34273  eulerpartlem1  34511  eulerpartgbij  34516  eulerpartlemmf  34519  coinflippv  34628  ballotlemoex  34630  reprval  34754  kur14lem9  35396  satfvsuclem1  35541  mpstval  35717  mclsrcl  35743  mclsval  35745  heibor1lem  38130  heibor  38142  idlval  38334  psubspset  40190  paddfval  40243  pclfvalN  40335  polfvalN  40350  psubclsetN  40382  docafvalN  41568  djafvalN  41580  dicval  41622  dochfval  41796  djhfval  41843  islpolN  41929  mzpclval  43157  eldiophb  43189  rpnnen3  43460  dfac11  43490  clsk1independent  44473  permaxpow  45436  dmvolsal  46774  ovnval  46969  smfresal  47216  sprbisymrel  47959  grtri  48416  uspgrex  48626  uspgrbisymrelALT  48631  lincop  48884  setrec2fun  50167  elpglem3  50188