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 2113  Vcvv 3437  𝒫 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 2115  ax-9 2123  ax-ext 2705  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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-pw 4551

This theorem is referenced by:  p0ex  5324  pp0ex  5326  ord3ex  5327  abexssex  7908  mptmpoopabbrd  8018  fnpm  8764  canth2  9050  dffi3  9322  r1sucg  9669  r1pwALT  9746  rankuni  9763  rankc2  9771  rankxpu  9776  rankmapu  9778  rankxplim  9779  r0weon  9910  aceq3lem  10018  dfac5lem4  10024  dfac5lem4OLD  10026  dfac2a  10028  dfac2b  10029  pwdju1  10089  ackbij2lem2  10137  ackbij2lem3  10138  fin23lem17  10236  domtriomlem  10340  axdc2lem  10346  axdc3lem  10348  axdclem2  10418  alephsucpw  10468  canthp1lem1  10550  gchac  10579  gruina  10716  npex  10884  nrex1  10962  pnfex  11172  mnfxr  11176  ixxex  13258  prdsvallem  17360  prdsds  17370  prdshom  17373  ismre  17494  fnmre  17495  fnmrc  17515  mrcfval  17516  mrisval  17538  wunfunc  17810  catcfuccl  18027  catcxpccl  18115  lubfval  18256  glbfval  18269  issubmgm  18612  issubm  18713  issubg  19041  cntzfval  19234  sylow1lem2  19513  lsmfval  19552  pj1fval  19608  issubrng  20464  issubrg  20488  rgspnval  20529  lssset  20868  lspfval  20908  islbs  21012  lbsext  21102  lbsexg  21103  sraval  21111  ocvfval  21605  cssval  21621  isobs  21659  islinds  21748  aspval  21812  istopon  22828  dmtopon  22839  fncld  22938  leordtval2  23128  cnpfval  23150  iscnp2  23155  kgenf  23457  xkoopn  23505  xkouni  23515  dfac14  23534  xkoccn  23535  prdstopn  23544  xkoco1cn  23573  xkoco2cn  23574  xkococn  23576  xkoinjcn  23603  isfbas  23745  uzrest  23813  acufl  23833  alexsubALTlem2  23964  tsmsval2  24046  ustfn  24118  ustn0  24137  ishtpy  24899  vitali  25542  madefi  27859  sspval  30705  shex  31194  hsupval  31316  fpwrelmap  32720  fpwrelmapffs  32721  dmvlsiga  34163  eulerpartlem1  34401  eulerpartgbij  34406  eulerpartlemmf  34409  coinflippv  34518  ballotlemoex  34520  reprval  34644  kur14lem9  35279  satfvsuclem1  35424  mpstval  35600  mclsrcl  35626  mclsval  35628  heibor1lem  37870  heibor  37882  idlval  38074  psubspset  39864  paddfval  39917  pclfvalN  40009  polfvalN  40024  psubclsetN  40056  docafvalN  41242  djafvalN  41254  dicval  41296  dochfval  41470  djhfval  41517  islpolN  41603  mzpclval  42843  eldiophb  42875  rpnnen3  43150  dfac11  43180  clsk1independent  44164  permaxpow  45127  dmvolsal  46469  ovnval  46664  smfresal  46911  sprbisymrel  47624  grtri  48065  uspgrex  48275  uspgrbisymrelALT  48280  lincop  48534  setrec2fun  49818  elpglem3  49839