Theorem pwex 5342

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  p0ex  5346  pp0ex  5348  ord3ex  5349  abexssex  7971  mptmpoopabbrd  8083  fnpm  8838  canth2  9133  dffi3  9407  r1sucg  9759  r1pwALT  9841  rankuni  9860  rankc2  9869  rankxpu  9874  rankmapu  9876  rankxplim  9877  setrec2fun  9954  r0weon  10072  aceq3lem  10180  dfac5lem4  10186  dfac2a  10189  dfac2b  10190  pwdju1  10250  ackbij2lem2  10298  ackbij2lem3  10299  fin23lem17  10397  domtriomlem  10501  axdc2lem  10507  axdc3lem  10509  axdclem2  10579  alephsucpw  10636  canthp1lem1  10718  gchac  10747  gruina  10884  npex  11052  nrex1  11130  pnfex  11343  mnfxr  11347  ixxex  13468  prdsvallem  17605  prdsds  17615  prdshom  17618  ismre  17740  fnmre  17741  fnmrc  17761  mrcfval  17762  mrisval  17784  wunfunc  18056  catcfuccl  18273  catcxpccl  18361  lubfval  18502  glbfval  18515  issubmgm  18871  issubm  18978  issubg  19316  cntzfval  19514  sylow1lem2  19793  lsmfval  19832  pj1fval  19888  issubrng  20779  issubrg  20803  rgspnval  20844  lssset  21188  lspfval  21228  islbs  21331  lbsext  21421  lbsexg  21422  sraval  21430  ocvfval  21952  cssval  21968  isobs  22006  islinds  22095  aspval  22160  istopon  23210  dmtopon  23221  fncld  23320  leordtval2  23510  cnpfval  23532  iscnp2  23537  kgenf  23840  xkoopn  23888  xkouni  23898  dfac14  23917  xkoccn  23918  prdstopn  23927  xkoco1cn  23956  xkoco2cn  23957  xkococn  23959  xkoinjcn  23986  isfbas  24128  uzrest  24196  acufl  24216  alexsubALTlem2  24347  tsmsval2  24429  ustfn  24501  ustn0  24520  ishtpy  25273  vitali  25914  sspval  31307  shex  31796  hsupval  31918  fpwrelmap  33307  fpwrelmapffs  33308  dmvlsiga  34743  eulerpartlem1  34982  eulerpartgbij  34987  eulerpartlemmf  34990  coinflippv  35099  ballotlemoex  35101  reprval  35222  kur14lem9  35948  satfvsuclem1  36093  mpstval  36269  mclsrcl  36295  mclsval  36297  heibor1lem  38711  heibor  38723  idlval  38915  psubspset  40769  paddfval  40822  pclfvalN  40914  polfvalN  40929  psubclsetN  40961  docafvalN  42147  djafvalN  42159  dicval  42201  dochfval  42375  djhfval  42422  islpolN  42508  mzpclval  43689  eldiophb  43721  rpnnen3  43992  dfac11  44022  clsk1independent  45005  permaxpow  45951  dmvolsal  47300  ovnval  47495  smfresal  47742  sprbisymrel  48525  grtri  48982  uspgrex  49192  uspgrbisymrelALT  49197  lincop  49464  elpglem3  50750