Theorem pwex 5349

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  𝒫 cpw 4560

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 2734  ax-sep 5255  ax-pow 5334

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-pw 4562

This theorem is used by:  p0ex  5353  pp0ex  5355  ord3ex  5356  abexssex  7971  mptmpoopabbrd  8084  fnpm  8837  canth2  9132  dffi3  9405  r1sucg  9755  r1pwALT  9832  rankuni  9849  rankc2  9857  rankxpu  9862  rankmapu  9864  rankxplim  9865  r0weon  10019  aceq3lem  10127  dfac5lem4  10133  dfac2a  10136  dfac2b  10137  pwdju1  10197  ackbij2lem2  10245  ackbij2lem3  10246  fin23lem17  10344  domtriomlem  10448  axdc2lem  10454  axdc3lem  10456  axdclem2  10526  alephsucpw  10583  canthp1lem1  10665  gchac  10694  gruina  10831  npex  10999  nrex1  11077  pnfex  11290  mnfxr  11294  ixxex  13413  prdsvallem  17545  prdsds  17555  prdshom  17558  ismre  17680  fnmre  17681  fnmrc  17701  mrcfval  17702  mrisval  17724  wunfunc  17996  catcfuccl  18213  catcxpccl  18301  lubfval  18442  glbfval  18455  issubmgm  18810  issubm  18917  issubg  19255  cntzfval  19453  sylow1lem2  19732  lsmfval  19771  pj1fval  19827  issubrng  20715  issubrg  20739  rgspnval  20780  lssset  21123  lspfval  21163  islbs  21266  lbsext  21356  lbsexg  21357  sraval  21365  ocvfval  21885  cssval  21901  isobs  21939  islinds  22028  aspval  22093  istopon  23143  dmtopon  23154  fncld  23253  leordtval2  23443  cnpfval  23465  iscnp2  23470  kgenf  23773  xkoopn  23821  xkouni  23831  dfac14  23850  xkoccn  23851  prdstopn  23860  xkoco1cn  23889  xkoco2cn  23890  xkococn  23892  xkoinjcn  23919  isfbas  24061  uzrest  24129  acufl  24149  alexsubALTlem2  24280  tsmsval2  24362  ustfn  24434  ustn0  24453  ishtpy  25206  vitali  25847  sspval  31212  shex  31701  hsupval  31823  fpwrelmap  33212  fpwrelmapffs  33213  dmvlsiga  34647  eulerpartlem1  34886  eulerpartgbij  34891  eulerpartlemmf  34894  coinflippv  35003  ballotlemoex  35005  reprval  35126  kur14lem9  35801  satfvsuclem1  35946  mpstval  36122  mclsrcl  36148  mclsval  36150  heibor1lem  38567  heibor  38579  idlval  38771  psubspset  40625  paddfval  40678  pclfvalN  40770  polfvalN  40785  psubclsetN  40817  docafvalN  42003  djafvalN  42015  dicval  42057  dochfval  42231  djhfval  42278  islpolN  42364  mzpclval  43578  eldiophb  43610  rpnnen3  43881  dfac11  43911  clsk1independent  44894  permaxpow  45840  dmvolsal  47182  ovnval  47377  smfresal  47624  sprbisymrel  48407  grtri  48864  uspgrex  49074  uspgrbisymrelALT  49079  lincop  49346  setrec2fun  50626  elpglem3  50647