Theorem pwex 5335

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-pow 5320

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  p0ex  5339  pp0ex  5341  ord3ex  5342  abexssex  7949  mptmpoopabbrd  8059  fnpm  8807  canth2  9094  dffi3  9382  r1sucg  9722  r1pwALT  9799  rankuni  9816  rankc2  9824  rankxpu  9829  rankmapu  9831  rankxplim  9832  r0weon  9965  aceq3lem  10073  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2a  10083  dfac2b  10084  pwdju1  10144  ackbij2lem2  10192  ackbij2lem3  10193  fin23lem17  10291  domtriomlem  10395  axdc2lem  10401  axdc3lem  10403  axdclem2  10473  alephsucpw  10523  canthp1lem1  10605  gchac  10634  gruina  10771  npex  10939  nrex1  11017  pnfex  11227  mnfxr  11231  ixxex  13317  prdsvallem  17417  prdsds  17427  prdshom  17430  ismre  17551  fnmre  17552  fnmrc  17568  mrcfval  17569  mrisval  17591  wunfunc  17863  catcfuccl  18080  catcxpccl  18168  lubfval  18309  glbfval  18322  issubmgm  18629  issubm  18730  issubg  19058  cntzfval  19252  sylow1lem2  19529  lsmfval  19568  pj1fval  19624  issubrng  20456  issubrg  20480  rgspnval  20521  lssset  20839  lspfval  20879  islbs  20983  lbsext  21073  lbsexg  21074  sraval  21082  ocvfval  21575  cssval  21591  isobs  21629  islinds  21718  aspval  21782  istopon  22799  dmtopon  22810  fncld  22909  leordtval2  23099  cnpfval  23121  iscnp2  23126  kgenf  23428  xkoopn  23476  xkouni  23486  dfac14  23505  xkoccn  23506  prdstopn  23515  xkoco1cn  23544  xkoco2cn  23545  xkococn  23547  xkoinjcn  23574  isfbas  23716  uzrest  23784  acufl  23804  alexsubALTlem2  23935  tsmsval2  24017  ustfn  24089  ustn0  24108  ishtpy  24871  vitali  25514  madefi  27824  sspval  30652  shex  31141  hsupval  31263  fpwrelmap  32656  fpwrelmapffs  32657  dmvlsiga  34119  eulerpartlem1  34358  eulerpartgbij  34363  eulerpartlemmf  34366  coinflippv  34475  ballotlemoex  34477  reprval  34601  kur14lem9  35201  satfvsuclem1  35346  mpstval  35522  mclsrcl  35548  mclsval  35550  heibor1lem  37803  heibor  37815  idlval  38007  psubspset  39738  paddfval  39791  pclfvalN  39883  polfvalN  39898  psubclsetN  39930  docafvalN  41116  djafvalN  41128  dicval  41170  dochfval  41344  djhfval  41391  islpolN  41477  mzpclval  42713  eldiophb  42745  rpnnen3  43021  dfac11  43051  clsk1independent  44035  permaxpow  44999  dmvolsal  46344  ovnval  46539  smfresal  46786  sprbisymrel  47500  grtri  47939  uspgrex  48138  uspgrbisymrelALT  48143  lincop  48397  setrec2fun  49681  elpglem3  49702