Theorem pwex 5380

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602

This theorem is referenced by:  p0ex  5384  pp0ex  5386  ord3ex  5387  abexssex  7995  mptmpoopabbrd  8105  fnpm  8874  canth2  9170  dffi3  9471  r1sucg  9809  r1pwALT  9886  rankuni  9903  rankc2  9911  rankxpu  9916  rankmapu  9918  rankxplim  9919  r0weon  10052  aceq3lem  10160  dfac5lem4  10166  dfac5lem4OLD  10168  dfac2a  10170  dfac2b  10171  pwdju1  10231  ackbij2lem2  10279  ackbij2lem3  10280  fin23lem17  10378  domtriomlem  10482  axdc2lem  10488  axdc3lem  10490  axdclem2  10560  alephsucpw  10610  canthp1lem1  10692  gchac  10721  gruina  10858  npex  11026  nrex1  11104  pnfex  11314  mnfxr  11318  ixxex  13398  prdsvallem  17499  prdsds  17509  prdshom  17512  ismre  17633  fnmre  17634  fnmrc  17650  mrcfval  17651  mrisval  17673  wunfunc  17946  catcfuccl  18163  catcxpccl  18252  lubfval  18395  glbfval  18408  issubmgm  18715  issubm  18816  issubg  19144  cntzfval  19338  sylow1lem2  19617  lsmfval  19656  pj1fval  19712  issubrng  20547  issubrg  20571  rgspnval  20612  lssset  20931  lspfval  20971  islbs  21075  lbsext  21165  lbsexg  21166  sraval  21174  ocvfval  21684  cssval  21700  isobs  21740  islinds  21829  aspval  21893  istopon  22918  dmtopon  22929  fncld  23030  leordtval2  23220  cnpfval  23242  iscnp2  23247  kgenf  23549  xkoopn  23597  xkouni  23607  dfac14  23626  xkoccn  23627  prdstopn  23636  xkoco1cn  23665  xkoco2cn  23666  xkococn  23668  xkoinjcn  23695  isfbas  23837  uzrest  23905  acufl  23925  alexsubALTlem2  24056  tsmsval2  24138  ustfn  24210  ustn0  24229  ishtpy  25004  vitali  25648  madefi  27950  sspval  30742  shex  31231  hsupval  31353  fpwrelmap  32744  fpwrelmapffs  32745  dmvlsiga  34130  eulerpartlem1  34369  eulerpartgbij  34374  eulerpartlemmf  34377  coinflippv  34486  ballotlemoex  34488  reprval  34625  kur14lem9  35219  satfvsuclem1  35364  mpstval  35540  mclsrcl  35566  mclsval  35568  heibor1lem  37816  heibor  37828  idlval  38020  psubspset  39746  paddfval  39799  pclfvalN  39891  polfvalN  39906  psubclsetN  39938  docafvalN  41124  djafvalN  41136  dicval  41178  dochfval  41352  djhfval  41399  islpolN  41485  mzpclval  42736  eldiophb  42768  rpnnen3  43044  dfac11  43074  clsk1independent  44059  dmvolsal  46361  ovnval  46556  smfresal  46803  sprbisymrel  47486  grtri  47907  uspgrex  48066  uspgrbisymrelALT  48071  lincop  48325  setrec2fun  49211  elpglem3  49232