Theorem pwex 5322

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  𝒫 cpw 4553

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-pow 5307

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-pw 4555

This theorem is referenced by:  p0ex  5326  pp0ex  5328  ord3ex  5329  abexssex  7912  mptmpoopabbrd  8022  fnpm  8768  canth2  9054  dffi3  9340  r1sucg  9684  r1pwALT  9761  rankuni  9778  rankc2  9786  rankxpu  9791  rankmapu  9793  rankxplim  9794  r0weon  9925  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2a  10043  dfac2b  10044  pwdju1  10104  ackbij2lem2  10152  ackbij2lem3  10153  fin23lem17  10251  domtriomlem  10355  axdc2lem  10361  axdc3lem  10363  axdclem2  10433  alephsucpw  10483  canthp1lem1  10565  gchac  10594  gruina  10731  npex  10899  nrex1  10977  pnfex  11187  mnfxr  11191  ixxex  13277  prdsvallem  17376  prdsds  17386  prdshom  17389  ismre  17510  fnmre  17511  fnmrc  17531  mrcfval  17532  mrisval  17554  wunfunc  17826  catcfuccl  18043  catcxpccl  18131  lubfval  18272  glbfval  18285  issubmgm  18594  issubm  18695  issubg  19023  cntzfval  19217  sylow1lem2  19496  lsmfval  19535  pj1fval  19591  issubrng  20450  issubrg  20474  rgspnval  20515  lssset  20854  lspfval  20894  islbs  20998  lbsext  21088  lbsexg  21089  sraval  21097  ocvfval  21591  cssval  21607  isobs  21645  islinds  21734  aspval  21798  istopon  22815  dmtopon  22826  fncld  22925  leordtval2  23115  cnpfval  23137  iscnp2  23142  kgenf  23444  xkoopn  23492  xkouni  23502  dfac14  23521  xkoccn  23522  prdstopn  23531  xkoco1cn  23560  xkoco2cn  23561  xkococn  23563  xkoinjcn  23590  isfbas  23732  uzrest  23800  acufl  23820  alexsubALTlem2  23951  tsmsval2  24033  ustfn  24105  ustn0  24124  ishtpy  24887  vitali  25530  madefi  27845  sspval  30685  shex  31174  hsupval  31296  fpwrelmap  32689  fpwrelmapffs  32690  dmvlsiga  34095  eulerpartlem1  34334  eulerpartgbij  34339  eulerpartlemmf  34342  coinflippv  34451  ballotlemoex  34453  reprval  34577  kur14lem9  35186  satfvsuclem1  35331  mpstval  35507  mclsrcl  35533  mclsval  35535  heibor1lem  37788  heibor  37800  idlval  37992  psubspset  39723  paddfval  39776  pclfvalN  39868  polfvalN  39883  psubclsetN  39915  docafvalN  41101  djafvalN  41113  dicval  41155  dochfval  41329  djhfval  41376  islpolN  41462  mzpclval  42698  eldiophb  42730  rpnnen3  43005  dfac11  43035  clsk1independent  44019  permaxpow  44983  dmvolsal  46328  ovnval  46523  smfresal  46770  sprbisymrel  47484  grtri  47925  uspgrex  48135  uspgrbisymrelALT  48140  lincop  48394  setrec2fun  49678  elpglem3  49699