Theorem pwex 5356

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  𝒫 cpw 4567

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-pw 4569

This theorem is used by:  p0ex  5360  pp0ex  5362  ord3ex  5363  abexssex  7976  mptmpoopabbrd  8087  fnpm  8840  canth2  9128  dffi3  9401  r1sucg  9751  r1pwALT  9828  rankuni  9845  rankc2  9853  rankxpu  9858  rankmapu  9860  rankxplim  9861  r0weon  10015  aceq3lem  10123  dfac5lem4  10129  dfac2a  10132  dfac2b  10133  pwdju1  10193  ackbij2lem2  10241  ackbij2lem3  10242  fin23lem17  10340  domtriomlem  10444  axdc2lem  10450  axdc3lem  10452  axdclem2  10522  alephsucpw  10573  canthp1lem1  10655  gchac  10684  gruina  10821  npex  10989  nrex1  11067  pnfex  11280  mnfxr  11284  ixxex  13401  prdsvallem  17532  prdsds  17542  prdshom  17545  ismre  17667  fnmre  17668  fnmrc  17688  mrcfval  17689  mrisval  17711  wunfunc  17983  catcfuccl  18200  catcxpccl  18288  lubfval  18429  glbfval  18442  issubmgm  18789  issubm  18892  issubg  19223  cntzfval  19421  sylow1lem2  19700  lsmfval  19739  pj1fval  19795  issubrng  20683  issubrg  20707  rgspnval  20748  lssset  21091  lspfval  21131  islbs  21234  lbsext  21324  lbsexg  21325  sraval  21333  ocvfval  21853  cssval  21869  isobs  21907  islinds  21996  aspval  22059  istopon  23106  dmtopon  23117  fncld  23216  leordtval2  23406  cnpfval  23428  iscnp2  23433  kgenf  23735  xkoopn  23783  xkouni  23793  dfac14  23812  xkoccn  23813  prdstopn  23822  xkoco1cn  23851  xkoco2cn  23852  xkococn  23854  xkoinjcn  23881  isfbas  24023  uzrest  24091  acufl  24111  alexsubALTlem2  24242  tsmsval2  24324  ustfn  24396  ustn0  24415  ishtpy  25168  vitali  25809  madefi  28143  sspval  31112  shex  31601  hsupval  31723  fpwrelmap  33115  fpwrelmapffs  33116  dmvlsiga  34550  eulerpartlem1  34789  eulerpartgbij  34794  eulerpartlemmf  34797  coinflippv  34906  ballotlemoex  34908  reprval  35029  kur14lem9  35727  satfvsuclem1  35872  mpstval  36048  mclsrcl  36074  mclsval  36076  heibor1lem  38501  heibor  38513  idlval  38705  psubspset  40559  paddfval  40612  pclfvalN  40704  polfvalN  40719  psubclsetN  40751  docafvalN  41937  djafvalN  41949  dicval  41991  dochfval  42165  djhfval  42212  islpolN  42298  mzpclval  43497  eldiophb  43529  rpnnen3  43800  dfac11  43830  clsk1independent  44813  permaxpow  45759  dmvolsal  47101  ovnval  47296  smfresal  47543  sprbisymrel  48289  grtri  48746  uspgrex  48956  uspgrbisymrelALT  48961  lincop  49229  setrec2fun  50511  elpglem3  50532