Theorem pwex 5281

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494  𝒫 cpw 4539

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 2793  ax-sep 5203  ax-pow 5266

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  p0ex  5285  pp0ex  5287  ord3ex  5288  abexssex  7671  fnpm  8414  canth2  8670  dffi3  8895  r1sucg  9198  r1pwALT  9275  rankuni  9292  rankc2  9300  rankxpu  9305  rankmapu  9307  rankxplim  9308  r0weon  9438  aceq3lem  9546  dfac5lem4  9552  dfac2a  9555  dfac2b  9556  pwdju1  9616  ackbij2lem2  9662  ackbij2lem3  9663  fin23lem17  9760  domtriomlem  9864  axdc2lem  9870  axdc3lem  9872  axdclem2  9942  alephsucpw  9992  canthp1lem1  10074  gchac  10103  gruina  10240  npex  10408  nrex1  10486  pnfex  10694  mnfxr  10698  ixxex  12750  prdsval  16728  prdsds  16737  prdshom  16740  ismre  16861  fnmre  16862  fnmrc  16878  mrcfval  16879  mrisval  16901  wunfunc  17169  catcfuccl  17369  catcxpccl  17457  lubfval  17588  glbfval  17601  issubm  17968  issubg  18279  cntzfval  18450  sylow1lem2  18724  lsmfval  18763  pj1fval  18820  issubrg  19535  lssset  19705  lspfval  19745  islbs  19848  lbsext  19935  lbsexg  19936  sraval  19948  aspval  20102  ocvfval  20810  cssval  20826  isobs  20864  islinds  20953  istopon  21520  dmtopon  21531  fncld  21630  leordtval2  21820  cnpfval  21842  iscnp2  21847  kgenf  22149  xkoopn  22197  xkouni  22207  dfac14  22226  xkoccn  22227  prdstopn  22236  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  isfbas  22437  uzrest  22505  acufl  22525  alexsubALTlem2  22656  tsmsval2  22738  ustfn  22810  ustn0  22829  ishtpy  23576  vitali  24214  sspval  28500  shex  28989  hsupval  29111  fpwrelmap  30469  fpwrelmapffs  30470  dmvlsiga  31388  eulerpartlem1  31625  eulerpartgbij  31630  eulerpartlemmf  31633  coinflippv  31741  ballotlemoex  31743  reprval  31881  kur14lem9  32461  satfvsuclem1  32606  mpstval  32782  mclsrcl  32808  mclsval  32810  heibor1lem  35102  heibor  35114  idlval  35306  psubspset  36895  paddfval  36948  pclfvalN  37040  polfvalN  37055  psubclsetN  37087  docafvalN  38273  djafvalN  38285  dicval  38327  dochfval  38501  djhfval  38548  islpolN  38634  mzpclval  39342  eldiophb  39374  rpnnen3  39649  dfac11  39682  rgspnval  39788  clsk1independent  40416  dmvolsal  42649  ovnval  42843  smfresal  43083  sprbisymrel  43681  uspgrex  44045  uspgrbisymrelALT  44050  issubmgm  44076  lincop  44483  setrec2fun  44815  vsetrec  44825  elpglem3  44835