Theorem pwex 5094

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

Syntax hints:   ∈ wcel 2107  Vcvv 3398  𝒫 cpw 4379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-sep 5019  ax-pow 5079

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400  df-in 3799  df-ss 3806  df-pw 4381

This theorem is referenced by:  p0ex  5097  pp0ex  5099  ord3ex  5100  abexssex  7429  fnpm  8150  canth2  8403  dffi3  8627  r1sucg  8931  r1pwALT  9008  rankuni  9025  rankc2  9033  rankxpu  9038  rankmapu  9040  rankxplim  9041  r0weon  9170  aceq3lem  9278  dfac5lem4  9284  dfac2a  9287  dfac2b  9288  dfac2OLD  9290  ackbij2lem2  9399  ackbij2lem3  9400  fin23lem17  9497  domtriomlem  9601  axdc2lem  9607  axdc3lem  9609  axdclem2  9679  alephsucpw  9729  canthp1lem1  9811  gchac  9840  gruina  9977  npex  10145  nrex1  10223  pnfex  10431  mnfxr  10436  ixxex  12502  prdsval  16505  prdsds  16514  prdshom  16517  ismre  16640  fnmre  16641  fnmrc  16657  mrcfval  16658  mrisval  16680  wunfunc  16948  catcfuccl  17148  catcxpccl  17237  lubfval  17368  glbfval  17381  issubm  17737  issubg  17982  cntzfval  18140  sylow1lem2  18402  lsmfval  18441  pj1fval  18495  issubrg  19176  lssset  19330  lspfval  19372  islbs  19475  lbsext  19564  lbsexg  19565  sraval  19577  aspval  19729  ocvfval  20413  cssval  20429  isobs  20467  islinds  20556  istopon  21128  dmtopon  21139  fncld  21238  leordtval2  21428  cnpfval  21450  iscnp2  21455  kgenf  21757  xkoopn  21805  xkouni  21815  dfac14  21834  xkoccn  21835  prdstopn  21844  xkoco1cn  21873  xkoco2cn  21874  xkococn  21876  xkoinjcn  21903  isfbas  22045  uzrest  22113  acufl  22133  alexsubALTlem2  22264  tsmsval2  22345  ustfn  22417  ustn0  22436  ishtpy  23183  vitali  23821  sspval  28154  shex  28645  hsupval  28769  fpwrelmap  30078  fpwrelmapffs  30079  isrnsigaOLD  30777  dmvlsiga  30794  eulerpartlem1  31031  eulerpartgbij  31036  eulerpartlemmf  31039  coinflippv  31148  ballotlemoex  31150  reprval  31294  kur14lem9  31799  mpstval  32035  mclsrcl  32061  mclsval  32063  heibor1lem  34237  heibor  34249  idlval  34441  psubspset  35903  paddfval  35956  pclfvalN  36048  polfvalN  36063  psubclsetN  36095  docafvalN  37281  djafvalN  37293  dicval  37335  dochfval  37509  djhfval  37556  islpolN  37642  mzpclval  38258  eldiophb  38290  rpnnen3  38568  dfac11  38601  rgspnval  38707  clsk1independent  39310  dmvolsal  41498  ovnval  41692  smfresal  41932  sprbisymrel  42448  uspgrex  42783  uspgrbisymrelALT  42788  issubmgm  42814  lincop  43222  setrec2fun  43554  vsetrec  43564  elpglem3  43574