Theorem pwex 5380

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

Syntax hints:   ∈ wcel 2098  Vcvv 3461  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-pow 5365

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-ss 3961  df-pw 4606

This theorem is referenced by:  p0ex  5384  pp0ex  5386  ord3ex  5387  abexssex  7975  mptmpoopabbrd  8085  fnpm  8853  canth2  9155  dffi3  9456  r1sucg  9794  r1pwALT  9871  rankuni  9888  rankc2  9896  rankxpu  9901  rankmapu  9903  rankxplim  9904  r0weon  10037  aceq3lem  10145  dfac5lem4  10151  dfac2a  10154  dfac2b  10155  pwdju1  10215  ackbij2lem2  10265  ackbij2lem3  10266  fin23lem17  10363  domtriomlem  10467  axdc2lem  10473  axdc3lem  10475  axdclem2  10545  alephsucpw  10595  canthp1lem1  10677  gchac  10706  gruina  10843  npex  11011  nrex1  11089  pnfex  11299  mnfxr  11303  ixxex  13370  prdsvallem  17439  prdsds  17449  prdshom  17452  ismre  17573  fnmre  17574  fnmrc  17590  mrcfval  17591  mrisval  17613  wunfunc  17890  wunfuncOLD  17891  catcfuccl  18111  catcfucclOLD  18112  catcxpccl  18201  catcxpcclOLD  18202  lubfval  18345  glbfval  18358  issubmgm  18665  issubm  18763  issubg  19089  cntzfval  19283  sylow1lem2  19566  lsmfval  19605  pj1fval  19661  issubrng  20496  issubrg  20522  lssset  20829  lspfval  20869  islbs  20973  lbsext  21063  lbsexg  21064  sraval  21072  ocvfval  21615  cssval  21631  isobs  21671  islinds  21760  aspval  21823  istopon  22858  dmtopon  22869  fncld  22970  leordtval2  23160  cnpfval  23182  iscnp2  23187  kgenf  23489  xkoopn  23537  xkouni  23547  dfac14  23566  xkoccn  23567  prdstopn  23576  xkoco1cn  23605  xkoco2cn  23606  xkococn  23608  xkoinjcn  23635  isfbas  23777  uzrest  23845  acufl  23865  alexsubALTlem2  23996  tsmsval2  24078  ustfn  24150  ustn0  24169  ishtpy  24942  vitali  25586  sspval  30605  shex  31094  hsupval  31216  fpwrelmap  32597  fpwrelmapffs  32598  dmvlsiga  33879  eulerpartlem1  34118  eulerpartgbij  34123  eulerpartlemmf  34126  coinflippv  34234  ballotlemoex  34236  reprval  34373  kur14lem9  34955  satfvsuclem1  35100  mpstval  35276  mclsrcl  35302  mclsval  35304  heibor1lem  37413  heibor  37425  idlval  37617  psubspset  39347  paddfval  39400  pclfvalN  39492  polfvalN  39507  psubclsetN  39539  docafvalN  40725  djafvalN  40737  dicval  40779  dochfval  40953  djhfval  41000  islpolN  41086  mzpclval  42287  eldiophb  42319  rpnnen3  42595  dfac11  42628  rgspnval  42734  clsk1independent  43618  dmvolsal  45872  ovnval  46067  smfresal  46314  sprbisymrel  46976  uspgrex  47398  uspgrbisymrelALT  47403  lincop  47662  setrec2fun  48309  elpglem3  48330