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

Theorem pwex 5273
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 5271 . 2 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
31, 2ax-mp 5 1 𝒫 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495  𝒫 cpw 4537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-pow 5258
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3497  df-in 3942  df-ss 3951  df-pw 4539
This theorem is referenced by:  p0ex  5276  pp0ex  5278  ord3ex  5279  abexssex  7662  fnpm  8404  canth2  8659  dffi3  8884  r1sucg  9187  r1pwALT  9264  rankuni  9281  rankc2  9289  rankxpu  9294  rankmapu  9296  rankxplim  9297  r0weon  9427  aceq3lem  9535  dfac5lem4  9541  dfac2a  9544  dfac2b  9545  pwdju1  9605  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  12739  prdsval  16718  prdsds  16727  prdshom  16730  ismre  16851  fnmre  16852  fnmrc  16868  mrcfval  16869  mrisval  16891  wunfunc  17159  catcfuccl  17359  catcxpccl  17447  lubfval  17578  glbfval  17591  issubm  17958  issubg  18219  cntzfval  18390  sylow1lem2  18655  lsmfval  18694  pj1fval  18751  issubrg  19466  lssset  19636  lspfval  19676  islbs  19779  lbsext  19866  lbsexg  19867  sraval  19879  aspval  20032  ocvfval  20740  cssval  20756  isobs  20794  islinds  20883  istopon  21450  dmtopon  21461  fncld  21560  leordtval2  21750  cnpfval  21772  iscnp2  21777  kgenf  22079  xkoopn  22127  xkouni  22137  dfac14  22156  xkoccn  22157  prdstopn  22166  xkoco1cn  22195  xkoco2cn  22196  xkococn  22198  xkoinjcn  22225  isfbas  22367  uzrest  22435  acufl  22455  alexsubALTlem2  22586  tsmsval2  22667  ustfn  22739  ustn0  22758  ishtpy  23505  vitali  24143  sspval  28428  shex  28917  hsupval  29039  fpwrelmap  30396  fpwrelmapffs  30397  dmvlsiga  31288  eulerpartlem1  31525  eulerpartgbij  31530  eulerpartlemmf  31533  coinflippv  31641  ballotlemoex  31643  reprval  31781  kur14lem9  32359  satfvsuclem1  32504  mpstval  32680  mclsrcl  32706  mclsval  32708  heibor1lem  34970  heibor  34982  idlval  35174  psubspset  36762  paddfval  36815  pclfvalN  36907  polfvalN  36922  psubclsetN  36954  docafvalN  38140  djafvalN  38152  dicval  38194  dochfval  38368  djhfval  38415  islpolN  38501  mzpclval  39202  eldiophb  39234  rpnnen3  39509  dfac11  39542  rgspnval  39648  clsk1independent  40276  dmvolsal  42510  ovnval  42704  smfresal  42944  sprbisymrel  43508  uspgrex  43872  uspgrbisymrelALT  43877  issubmgm  43903  lincop  44361  setrec2fun  44693  vsetrec  44703  elpglem3  44713
  Copyright terms: Public domain W3C validator