Theorem pwex 5385

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-pow 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-pw 4606

This theorem is referenced by:  p0ex  5389  pp0ex  5391  ord3ex  5392  abexssex  7993  mptmpoopabbrd  8103  fnpm  8872  canth2  9168  dffi3  9468  r1sucg  9806  r1pwALT  9883  rankuni  9900  rankc2  9908  rankxpu  9913  rankmapu  9915  rankxplim  9916  r0weon  10049  aceq3lem  10157  dfac5lem4  10163  dfac5lem4OLD  10165  dfac2a  10167  dfac2b  10168  pwdju1  10228  ackbij2lem2  10276  ackbij2lem3  10277  fin23lem17  10375  domtriomlem  10479  axdc2lem  10485  axdc3lem  10487  axdclem2  10557  alephsucpw  10607  canthp1lem1  10689  gchac  10718  gruina  10855  npex  11023  nrex1  11101  pnfex  11311  mnfxr  11315  ixxex  13394  prdsvallem  17500  prdsds  17510  prdshom  17513  ismre  17634  fnmre  17635  fnmrc  17651  mrcfval  17652  mrisval  17674  wunfunc  17951  wunfuncOLD  17952  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  lubfval  18407  glbfval  18420  issubmgm  18727  issubm  18828  issubg  19156  cntzfval  19350  sylow1lem2  19631  lsmfval  19670  pj1fval  19726  issubrng  20563  issubrg  20587  rgspnval  20628  lssset  20948  lspfval  20988  islbs  21092  lbsext  21182  lbsexg  21183  sraval  21191  ocvfval  21701  cssval  21717  isobs  21757  islinds  21846  aspval  21910  istopon  22933  dmtopon  22944  fncld  23045  leordtval2  23235  cnpfval  23257  iscnp2  23262  kgenf  23564  xkoopn  23612  xkouni  23622  dfac14  23641  xkoccn  23642  prdstopn  23651  xkoco1cn  23680  xkoco2cn  23681  xkococn  23683  xkoinjcn  23710  isfbas  23852  uzrest  23920  acufl  23940  alexsubALTlem2  24071  tsmsval2  24153  ustfn  24225  ustn0  24244  ishtpy  25017  vitali  25661  madefi  27964  sspval  30751  shex  31240  hsupval  31362  fpwrelmap  32750  fpwrelmapffs  32751  dmvlsiga  34109  eulerpartlem1  34348  eulerpartgbij  34353  eulerpartlemmf  34356  coinflippv  34464  ballotlemoex  34466  reprval  34603  kur14lem9  35198  satfvsuclem1  35343  mpstval  35519  mclsrcl  35545  mclsval  35547  heibor1lem  37795  heibor  37807  idlval  37999  psubspset  39726  paddfval  39779  pclfvalN  39871  polfvalN  39886  psubclsetN  39918  docafvalN  41104  djafvalN  41116  dicval  41158  dochfval  41332  djhfval  41379  islpolN  41465  mzpclval  42712  eldiophb  42744  rpnnen3  43020  dfac11  43050  clsk1independent  44035  dmvolsal  46301  ovnval  46496  smfresal  46743  sprbisymrel  47423  grtri  47844  uspgrex  47993  uspgrbisymrelALT  47998  lincop  48253  setrec2fun  48922  elpglem3  48943