Theorem pwex 5283

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  𝒫 cpw 4541

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-pow 5268

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  p0ex  5287  pp0ex  5289  ord3ex  5290  abexssex  7673  fnpm  8416  canth2  8672  dffi3  8897  r1sucg  9200  r1pwALT  9277  rankuni  9294  rankc2  9302  rankxpu  9307  rankmapu  9309  rankxplim  9310  r0weon  9440  aceq3lem  9548  dfac5lem4  9554  dfac2a  9557  dfac2b  9558  pwdju1  9618  ackbij2lem2  9664  ackbij2lem3  9665  fin23lem17  9762  domtriomlem  9866  axdc2lem  9872  axdc3lem  9874  axdclem2  9944  alephsucpw  9994  canthp1lem1  10076  gchac  10105  gruina  10242  npex  10410  nrex1  10488  pnfex  10696  mnfxr  10700  ixxex  12752  prdsval  16730  prdsds  16739  prdshom  16742  ismre  16863  fnmre  16864  fnmrc  16880  mrcfval  16881  mrisval  16903  wunfunc  17171  catcfuccl  17371  catcxpccl  17459  lubfval  17590  glbfval  17603  issubm  17970  issubg  18281  cntzfval  18452  sylow1lem2  18726  lsmfval  18765  pj1fval  18822  issubrg  19537  lssset  19707  lspfval  19747  islbs  19850  lbsext  19937  lbsexg  19938  sraval  19950  aspval  20104  ocvfval  20812  cssval  20828  isobs  20866  islinds  20955  istopon  21522  dmtopon  21533  fncld  21632  leordtval2  21822  cnpfval  21844  iscnp2  21849  kgenf  22151  xkoopn  22199  xkouni  22209  dfac14  22228  xkoccn  22229  prdstopn  22238  xkoco1cn  22267  xkoco2cn  22268  xkococn  22270  xkoinjcn  22297  isfbas  22439  uzrest  22507  acufl  22527  alexsubALTlem2  22658  tsmsval2  22740  ustfn  22812  ustn0  22831  ishtpy  23578  vitali  24216  sspval  28502  shex  28991  hsupval  29113  fpwrelmap  30471  fpwrelmapffs  30472  dmvlsiga  31390  eulerpartlem1  31627  eulerpartgbij  31632  eulerpartlemmf  31635  coinflippv  31743  ballotlemoex  31745  reprval  31883  kur14lem9  32463  satfvsuclem1  32608  mpstval  32784  mclsrcl  32810  mclsval  32812  heibor1lem  35089  heibor  35101  idlval  35293  psubspset  36882  paddfval  36935  pclfvalN  37027  polfvalN  37042  psubclsetN  37074  docafvalN  38260  djafvalN  38272  dicval  38314  dochfval  38488  djhfval  38535  islpolN  38621  mzpclval  39329  eldiophb  39361  rpnnen3  39636  dfac11  39669  rgspnval  39775  clsk1independent  40403  dmvolsal  42636  ovnval  42830  smfresal  43070  sprbisymrel  43668  uspgrex  44032  uspgrbisymrelALT  44037  issubmgm  44063  lincop  44470  setrec2fun  44802  vsetrec  44812  elpglem3  44822