Theorem pwex 5246

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  𝒫 cpw 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  p0ex  5250  pp0ex  5252  ord3ex  5253  abexssex  7653  fnpm  8397  canth2  8654  dffi3  8879  r1sucg  9182  r1pwALT  9259  rankuni  9276  rankc2  9284  rankxpu  9289  rankmapu  9291  rankxplim  9292  r0weon  9423  aceq3lem  9531  dfac5lem4  9537  dfac2a  9540  dfac2b  9541  pwdju1  9601  ackbij2lem2  9651  ackbij2lem3  9652  fin23lem17  9749  domtriomlem  9853  axdc2lem  9859  axdc3lem  9861  axdclem2  9931  alephsucpw  9981  canthp1lem1  10063  gchac  10092  gruina  10229  npex  10397  nrex1  10475  pnfex  10683  mnfxr  10687  ixxex  12737  prdsval  16720  prdsds  16729  prdshom  16732  ismre  16853  fnmre  16854  fnmrc  16870  mrcfval  16871  mrisval  16893  wunfunc  17161  catcfuccl  17361  catcxpccl  17449  lubfval  17580  glbfval  17593  issubm  17960  issubg  18271  cntzfval  18442  sylow1lem2  18716  lsmfval  18755  pj1fval  18812  issubrg  19528  lssset  19698  lspfval  19738  islbs  19841  lbsext  19928  lbsexg  19929  sraval  19941  ocvfval  20355  cssval  20371  isobs  20409  islinds  20498  aspval  20559  istopon  21517  dmtopon  21528  fncld  21627  leordtval2  21817  cnpfval  21839  iscnp2  21844  kgenf  22146  xkoopn  22194  xkouni  22204  dfac14  22223  xkoccn  22224  prdstopn  22233  xkoco1cn  22262  xkoco2cn  22263  xkococn  22265  xkoinjcn  22292  isfbas  22434  uzrest  22502  acufl  22522  alexsubALTlem2  22653  tsmsval2  22735  ustfn  22807  ustn0  22826  ishtpy  23577  vitali  24217  sspval  28506  shex  28995  hsupval  29117  fpwrelmap  30495  fpwrelmapffs  30496  dmvlsiga  31498  eulerpartlem1  31735  eulerpartgbij  31740  eulerpartlemmf  31743  coinflippv  31851  ballotlemoex  31853  reprval  31991  kur14lem9  32574  satfvsuclem1  32719  mpstval  32895  mclsrcl  32921  mclsval  32923  heibor1lem  35247  heibor  35259  idlval  35451  psubspset  37040  paddfval  37093  pclfvalN  37185  polfvalN  37200  psubclsetN  37232  docafvalN  38418  djafvalN  38430  dicval  38472  dochfval  38646  djhfval  38693  islpolN  38779  mzpclval  39666  eldiophb  39698  rpnnen3  39973  dfac11  40006  rgspnval  40112  clsk1independent  40749  dmvolsal  42986  ovnval  43180  smfresal  43420  sprbisymrel  44016  uspgrex  44378  uspgrbisymrelALT  44383  issubmgm  44409  lincop  44817  setrec2fun  45222  vsetrec  45232  elpglem3  45242