MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwex Structured version   Visualization version   GIF version

Theorem pwex 5268
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
StepHypRef Expression
1 pwex.1 . 2 𝐴 ∈ V
2 pwexg 5266 . 2 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
31, 2ax-mp 5 1 𝒫 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  Vcvv 3480  𝒫 cpw 4522
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-pow 5253
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 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-pw 4524
This theorem is referenced by:  p0ex  5272  pp0ex  5274  ord3ex  5275  abexssex  7666  fnpm  8410  canth2  8667  dffi3  8892  r1sucg  9195  r1pwALT  9272  rankuni  9289  rankc2  9297  rankxpu  9302  rankmapu  9304  rankxplim  9305  r0weon  9436  aceq3lem  9544  dfac5lem4  9550  dfac2a  9553  dfac2b  9554  pwdju1  9614  ackbij2lem2  9660  ackbij2lem3  9661  fin23lem17  9758  domtriomlem  9862  axdc2lem  9868  axdc3lem  9870  axdclem2  9940  alephsucpw  9990  canthp1lem1  10072  gchac  10101  gruina  10238  npex  10406  nrex1  10484  pnfex  10692  mnfxr  10696  ixxex  12746  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  23580  vitali  24220  sspval  28509  shex  28998  hsupval  29120  fpwrelmap  30480  fpwrelmapffs  30481  dmvlsiga  31445  eulerpartlem1  31682  eulerpartgbij  31687  eulerpartlemmf  31690  coinflippv  31798  ballotlemoex  31800  reprval  31938  kur14lem9  32518  satfvsuclem1  32663  mpstval  32839  mclsrcl  32865  mclsval  32867  heibor1lem  35192  heibor  35204  idlval  35396  psubspset  36985  paddfval  37038  pclfvalN  37130  polfvalN  37145  psubclsetN  37177  docafvalN  38363  djafvalN  38375  dicval  38417  dochfval  38591  djhfval  38638  islpolN  38724  mzpclval  39582  eldiophb  39614  rpnnen3  39889  dfac11  39922  rgspnval  40028  clsk1independent  40668  dmvolsal  42912  ovnval  43106  smfresal  43346  sprbisymrel  43942  uspgrex  44304  uspgrbisymrelALT  44309  issubmgm  44335  lincop  44743  setrec2fun  45148  vsetrec  45158  elpglem3  45168
  Copyright terms: Public domain W3C validator