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 2106  Vcvv 3432  𝒫 cpw 4533

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-pow 5288

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  p0ex  5307  pp0ex  5309  ord3ex  5310  abexssex  7813  fnpm  8623  canth2  8917  dffi3  9190  r1sucg  9527  r1pwALT  9604  rankuni  9621  rankc2  9629  rankxpu  9634  rankmapu  9636  rankxplim  9637  r0weon  9768  aceq3lem  9876  dfac5lem4  9882  dfac2a  9885  dfac2b  9886  pwdju1  9946  ackbij2lem2  9996  ackbij2lem3  9997  fin23lem17  10094  domtriomlem  10198  axdc2lem  10204  axdc3lem  10206  axdclem2  10276  alephsucpw  10326  canthp1lem1  10408  gchac  10437  gruina  10574  npex  10742  nrex1  10820  pnfex  11028  mnfxr  11032  ixxex  13090  prdsvallem  17165  prdsds  17175  prdshom  17178  ismre  17299  fnmre  17300  fnmrc  17316  mrcfval  17317  mrisval  17339  wunfunc  17614  wunfuncOLD  17615  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  lubfval  18068  glbfval  18081  issubm  18442  issubg  18755  cntzfval  18926  sylow1lem2  19204  lsmfval  19243  pj1fval  19300  issubrg  20024  lssset  20195  lspfval  20235  islbs  20338  lbsext  20425  lbsexg  20426  sraval  20438  ocvfval  20871  cssval  20887  isobs  20927  islinds  21016  aspval  21077  istopon  22061  dmtopon  22072  fncld  22173  leordtval2  22363  cnpfval  22385  iscnp2  22390  kgenf  22692  xkoopn  22740  xkouni  22750  dfac14  22769  xkoccn  22770  prdstopn  22779  xkoco1cn  22808  xkoco2cn  22809  xkococn  22811  xkoinjcn  22838  isfbas  22980  uzrest  23048  acufl  23068  alexsubALTlem2  23199  tsmsval2  23281  ustfn  23353  ustn0  23372  ishtpy  24135  vitali  24777  sspval  29085  shex  29574  hsupval  29696  fpwrelmap  31068  fpwrelmapffs  31069  dmvlsiga  32097  eulerpartlem1  32334  eulerpartgbij  32339  eulerpartlemmf  32342  coinflippv  32450  ballotlemoex  32452  reprval  32590  kur14lem9  33176  satfvsuclem1  33321  mpstval  33497  mclsrcl  33523  mclsval  33525  heibor1lem  35967  heibor  35979  idlval  36171  psubspset  37758  paddfval  37811  pclfvalN  37903  polfvalN  37918  psubclsetN  37950  docafvalN  39136  djafvalN  39148  dicval  39190  dochfval  39364  djhfval  39411  islpolN  39497  mzpclval  40547  eldiophb  40579  rpnnen3  40854  dfac11  40887  rgspnval  40993  clsk1independent  41656  dmvolsal  43885  ovnval  44079  smfresal  44322  sprbisymrel  44951  uspgrex  45312  uspgrbisymrelALT  45317  issubmgm  45343  lincop  45749  setrec2fun  46398  vsetrec  46408  elpglem3  46418