Theorem pwex 5303

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

Syntax hints:   ∈ wcel 2107  Vcvv 3427  𝒫 cpw 4535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5223  ax-pow 5288

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3429  df-in 3895  df-ss 3905  df-pw 4537

This theorem is referenced by:  p0ex  5307  pp0ex  5309  ord3ex  5310  abexssex  7791  fnpm  8586  canth2  8871  dffi3  9136  r1sucg  9474  r1pwALT  9551  rankuni  9568  rankc2  9576  rankxpu  9581  rankmapu  9583  rankxplim  9584  r0weon  9715  aceq3lem  9823  dfac5lem4  9829  dfac2a  9832  dfac2b  9833  pwdju1  9893  ackbij2lem2  9943  ackbij2lem3  9944  fin23lem17  10041  domtriomlem  10145  axdc2lem  10151  axdc3lem  10153  axdclem2  10223  alephsucpw  10273  canthp1lem1  10355  gchac  10384  gruina  10521  npex  10689  nrex1  10767  pnfex  10975  mnfxr  10979  ixxex  13035  prdsvallem  17109  prdsds  17119  prdshom  17122  ismre  17243  fnmre  17244  fnmrc  17260  mrcfval  17261  mrisval  17283  wunfunc  17558  wunfuncOLD  17559  catcfuccl  17778  catcfucclOLD  17779  catcxpccl  17868  catcxpcclOLD  17869  lubfval  18012  glbfval  18025  issubm  18386  issubg  18699  cntzfval  18870  sylow1lem2  19148  lsmfval  19187  pj1fval  19244  issubrg  19968  lssset  20139  lspfval  20179  islbs  20282  lbsext  20369  lbsexg  20370  sraval  20382  ocvfval  20815  cssval  20831  isobs  20871  islinds  20960  aspval  21021  istopon  22005  dmtopon  22016  fncld  22117  leordtval2  22307  cnpfval  22329  iscnp2  22334  kgenf  22636  xkoopn  22684  xkouni  22694  dfac14  22713  xkoccn  22714  prdstopn  22723  xkoco1cn  22752  xkoco2cn  22753  xkococn  22755  xkoinjcn  22782  isfbas  22924  uzrest  22992  acufl  23012  alexsubALTlem2  23143  tsmsval2  23225  ustfn  23297  ustn0  23316  ishtpy  24079  vitali  24720  sspval  29026  shex  29515  hsupval  29637  fpwrelmap  31010  fpwrelmapffs  31011  dmvlsiga  32039  eulerpartlem1  32276  eulerpartgbij  32281  eulerpartlemmf  32284  coinflippv  32392  ballotlemoex  32394  reprval  32532  kur14lem9  33118  satfvsuclem1  33263  mpstval  33439  mclsrcl  33465  mclsval  33467  heibor1lem  35936  heibor  35948  idlval  36140  psubspset  37727  paddfval  37780  pclfvalN  37872  polfvalN  37887  psubclsetN  37919  docafvalN  39105  djafvalN  39117  dicval  39159  dochfval  39333  djhfval  39380  islpolN  39466  mzpclval  40505  eldiophb  40537  rpnnen3  40812  dfac11  40845  rgspnval  40951  clsk1independent  41587  dmvolsal  43817  ovnval  44011  smfresal  44251  sprbisymrel  44881  uspgrex  45242  uspgrbisymrelALT  45247  issubmgm  45273  lincop  45679  setrec2fun  46328  vsetrec  46338  elpglem3  46348