Theorem pwex 5350

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  𝒫 cpw 4575

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pow 5335

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-pw 4577

This theorem is referenced by:  p0ex  5354  pp0ex  5356  ord3ex  5357  abexssex  7967  mptmpoopabbrd  8077  fnpm  8846  canth2  9142  dffi3  9441  r1sucg  9781  r1pwALT  9858  rankuni  9875  rankc2  9883  rankxpu  9888  rankmapu  9890  rankxplim  9891  r0weon  10024  aceq3lem  10132  dfac5lem4  10138  dfac5lem4OLD  10140  dfac2a  10142  dfac2b  10143  pwdju1  10203  ackbij2lem2  10251  ackbij2lem3  10252  fin23lem17  10350  domtriomlem  10454  axdc2lem  10460  axdc3lem  10462  axdclem2  10532  alephsucpw  10582  canthp1lem1  10664  gchac  10693  gruina  10830  npex  10998  nrex1  11076  pnfex  11286  mnfxr  11290  ixxex  13371  prdsvallem  17466  prdsds  17476  prdshom  17479  ismre  17600  fnmre  17601  fnmrc  17617  mrcfval  17618  mrisval  17640  wunfunc  17912  catcfuccl  18129  catcxpccl  18217  lubfval  18358  glbfval  18371  issubmgm  18678  issubm  18779  issubg  19107  cntzfval  19301  sylow1lem2  19578  lsmfval  19617  pj1fval  19673  issubrng  20505  issubrg  20529  rgspnval  20570  lssset  20888  lspfval  20928  islbs  21032  lbsext  21122  lbsexg  21123  sraval  21131  ocvfval  21624  cssval  21640  isobs  21678  islinds  21767  aspval  21831  istopon  22848  dmtopon  22859  fncld  22958  leordtval2  23148  cnpfval  23170  iscnp2  23175  kgenf  23477  xkoopn  23525  xkouni  23535  dfac14  23554  xkoccn  23555  prdstopn  23564  xkoco1cn  23593  xkoco2cn  23594  xkococn  23596  xkoinjcn  23623  isfbas  23765  uzrest  23833  acufl  23853  alexsubALTlem2  23984  tsmsval2  24066  ustfn  24138  ustn0  24157  ishtpy  24920  vitali  25564  madefi  27867  sspval  30650  shex  31139  hsupval  31261  fpwrelmap  32656  fpwrelmapffs  32657  dmvlsiga  34106  eulerpartlem1  34345  eulerpartgbij  34350  eulerpartlemmf  34353  coinflippv  34462  ballotlemoex  34464  reprval  34588  kur14lem9  35182  satfvsuclem1  35327  mpstval  35503  mclsrcl  35529  mclsval  35531  heibor1lem  37779  heibor  37791  idlval  37983  psubspset  39709  paddfval  39762  pclfvalN  39854  polfvalN  39869  psubclsetN  39901  docafvalN  41087  djafvalN  41099  dicval  41141  dochfval  41315  djhfval  41362  islpolN  41448  mzpclval  42695  eldiophb  42727  rpnnen3  43003  dfac11  43033  clsk1independent  44017  permaxpow  44982  dmvolsal  46323  ovnval  46518  smfresal  46765  sprbisymrel  47461  grtri  47900  uspgrex  48073  uspgrbisymrelALT  48078  lincop  48332  setrec2fun  49504  elpglem3  49525