Theorem pwex 5325

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pow 5310

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556

This theorem is referenced by:  p0ex  5329  pp0ex  5331  ord3ex  5332  abexssex  7914  mptmpoopabbrd  8024  fnpm  8771  canth2  9058  dffi3  9334  r1sucg  9681  r1pwALT  9758  rankuni  9775  rankc2  9783  rankxpu  9788  rankmapu  9790  rankxplim  9791  r0weon  9922  aceq3lem  10030  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2a  10040  dfac2b  10041  pwdju1  10101  ackbij2lem2  10149  ackbij2lem3  10150  fin23lem17  10248  domtriomlem  10352  axdc2lem  10358  axdc3lem  10360  axdclem2  10430  alephsucpw  10481  canthp1lem1  10563  gchac  10592  gruina  10729  npex  10897  nrex1  10975  pnfex  11185  mnfxr  11189  ixxex  13272  prdsvallem  17374  prdsds  17384  prdshom  17387  ismre  17509  fnmre  17510  fnmrc  17530  mrcfval  17531  mrisval  17553  wunfunc  17825  catcfuccl  18042  catcxpccl  18130  lubfval  18271  glbfval  18284  issubmgm  18627  issubm  18728  issubg  19056  cntzfval  19249  sylow1lem2  19528  lsmfval  19567  pj1fval  19623  issubrng  20480  issubrg  20504  rgspnval  20545  lssset  20884  lspfval  20924  islbs  21028  lbsext  21118  lbsexg  21119  sraval  21127  ocvfval  21621  cssval  21637  isobs  21675  islinds  21764  aspval  21828  istopon  22856  dmtopon  22867  fncld  22966  leordtval2  23156  cnpfval  23178  iscnp2  23183  kgenf  23485  xkoopn  23533  xkouni  23543  dfac14  23562  xkoccn  23563  prdstopn  23572  xkoco1cn  23601  xkoco2cn  23602  xkococn  23604  xkoinjcn  23631  isfbas  23773  uzrest  23841  acufl  23861  alexsubALTlem2  23992  tsmsval2  24074  ustfn  24146  ustn0  24165  ishtpy  24927  vitali  25570  madefi  27909  sspval  30798  shex  31287  hsupval  31409  fpwrelmap  32812  fpwrelmapffs  32813  dmvlsiga  34286  eulerpartlem1  34524  eulerpartgbij  34529  eulerpartlemmf  34532  coinflippv  34641  ballotlemoex  34643  reprval  34767  kur14lem9  35408  satfvsuclem1  35553  mpstval  35729  mclsrcl  35755  mclsval  35757  heibor1lem  38006  heibor  38018  idlval  38210  psubspset  40000  paddfval  40053  pclfvalN  40145  polfvalN  40160  psubclsetN  40192  docafvalN  41378  djafvalN  41390  dicval  41432  dochfval  41606  djhfval  41653  islpolN  41739  mzpclval  42963  eldiophb  42995  rpnnen3  43270  dfac11  43300  clsk1independent  44283  permaxpow  45246  dmvolsal  46586  ovnval  46781  smfresal  47028  sprbisymrel  47741  grtri  48182  uspgrex  48392  uspgrbisymrelALT  48397  lincop  48650  setrec2fun  49933  elpglem3  49954