Theorem pwex 5398

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  p0ex  5402  pp0ex  5404  ord3ex  5405  abexssex  8011  mptmpoopabbrd  8121  fnpm  8892  canth2  9196  dffi3  9500  r1sucg  9838  r1pwALT  9915  rankuni  9932  rankc2  9940  rankxpu  9945  rankmapu  9947  rankxplim  9948  r0weon  10081  aceq3lem  10189  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2a  10199  dfac2b  10200  pwdju1  10260  ackbij2lem2  10308  ackbij2lem3  10309  fin23lem17  10407  domtriomlem  10511  axdc2lem  10517  axdc3lem  10519  axdclem2  10589  alephsucpw  10639  canthp1lem1  10721  gchac  10750  gruina  10887  npex  11055  nrex1  11133  pnfex  11343  mnfxr  11347  ixxex  13418  prdsvallem  17514  prdsds  17524  prdshom  17527  ismre  17648  fnmre  17649  fnmrc  17665  mrcfval  17666  mrisval  17688  wunfunc  17965  wunfuncOLD  17966  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  lubfval  18420  glbfval  18433  issubmgm  18740  issubm  18838  issubg  19166  cntzfval  19360  sylow1lem2  19641  lsmfval  19680  pj1fval  19736  issubrng  20573  issubrg  20599  lssset  20954  lspfval  20994  islbs  21098  lbsext  21188  lbsexg  21189  sraval  21197  ocvfval  21707  cssval  21723  isobs  21763  islinds  21852  aspval  21916  istopon  22939  dmtopon  22950  fncld  23051  leordtval2  23241  cnpfval  23263  iscnp2  23268  kgenf  23570  xkoopn  23618  xkouni  23628  dfac14  23647  xkoccn  23648  prdstopn  23657  xkoco1cn  23686  xkoco2cn  23687  xkococn  23689  xkoinjcn  23716  isfbas  23858  uzrest  23926  acufl  23946  alexsubALTlem2  24077  tsmsval2  24159  ustfn  24231  ustn0  24250  ishtpy  25023  vitali  25667  madefi  27968  sspval  30755  shex  31244  hsupval  31366  fpwrelmap  32747  fpwrelmapffs  32748  dmvlsiga  34093  eulerpartlem1  34332  eulerpartgbij  34337  eulerpartlemmf  34340  coinflippv  34448  ballotlemoex  34450  reprval  34587  kur14lem9  35182  satfvsuclem1  35327  mpstval  35503  mclsrcl  35529  mclsval  35531  heibor1lem  37769  heibor  37781  idlval  37973  psubspset  39701  paddfval  39754  pclfvalN  39846  polfvalN  39861  psubclsetN  39893  docafvalN  41079  djafvalN  41091  dicval  41133  dochfval  41307  djhfval  41354  islpolN  41440  mzpclval  42681  eldiophb  42713  rpnnen3  42989  dfac11  43019  rgspnval  43125  clsk1independent  44008  dmvolsal  46267  ovnval  46462  smfresal  46709  sprbisymrel  47373  grtri  47791  uspgrex  47873  uspgrbisymrelALT  47878  lincop  48137  setrec2fun  48784  elpglem3  48805