Theorem pwex 5379

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-pow 5364

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  p0ex  5383  pp0ex  5385  ord3ex  5386  abexssex  7957  fnpm  8828  canth2  9130  dffi3  9426  r1sucg  9764  r1pwALT  9841  rankuni  9858  rankc2  9866  rankxpu  9871  rankmapu  9873  rankxplim  9874  r0weon  10007  aceq3lem  10115  dfac5lem4  10121  dfac2a  10124  dfac2b  10125  pwdju1  10185  ackbij2lem2  10235  ackbij2lem3  10236  fin23lem17  10333  domtriomlem  10437  axdc2lem  10443  axdc3lem  10445  axdclem2  10515  alephsucpw  10565  canthp1lem1  10647  gchac  10676  gruina  10813  npex  10981  nrex1  11059  pnfex  11267  mnfxr  11271  ixxex  13335  prdsvallem  17400  prdsds  17410  prdshom  17413  ismre  17534  fnmre  17535  fnmrc  17551  mrcfval  17552  mrisval  17574  wunfunc  17849  wunfuncOLD  17850  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  lubfval  18303  glbfval  18316  issubm  18684  issubg  19006  cntzfval  19184  sylow1lem2  19467  lsmfval  19506  pj1fval  19562  issubrg  20319  lssset  20544  lspfval  20584  islbs  20687  lbsext  20776  lbsexg  20777  sraval  20789  ocvfval  21219  cssval  21235  isobs  21275  islinds  21364  aspval  21427  istopon  22414  dmtopon  22425  fncld  22526  leordtval2  22716  cnpfval  22738  iscnp2  22743  kgenf  23045  xkoopn  23093  xkouni  23103  dfac14  23122  xkoccn  23123  prdstopn  23132  xkoco1cn  23161  xkoco2cn  23162  xkococn  23164  xkoinjcn  23191  isfbas  23333  uzrest  23401  acufl  23421  alexsubALTlem2  23552  tsmsval2  23634  ustfn  23706  ustn0  23725  ishtpy  24488  vitali  25130  sspval  29976  shex  30465  hsupval  30587  fpwrelmap  31958  fpwrelmapffs  31959  dmvlsiga  33127  eulerpartlem1  33366  eulerpartgbij  33371  eulerpartlemmf  33374  coinflippv  33482  ballotlemoex  33484  reprval  33622  kur14lem9  34205  satfvsuclem1  34350  mpstval  34526  mclsrcl  34552  mclsval  34554  heibor1lem  36677  heibor  36689  idlval  36881  psubspset  38615  paddfval  38668  pclfvalN  38760  polfvalN  38775  psubclsetN  38807  docafvalN  39993  djafvalN  40005  dicval  40047  dochfval  40221  djhfval  40268  islpolN  40354  mzpclval  41463  eldiophb  41495  rpnnen3  41771  dfac11  41804  rgspnval  41910  clsk1independent  42797  dmvolsal  45062  ovnval  45257  smfresal  45504  sprbisymrel  46167  uspgrex  46528  uspgrbisymrelALT  46533  issubmgm  46559  issubrng  46726  lincop  47089  setrec2fun  47737  elpglem3  47758