Theorem pwex 5347

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  𝒫 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  p0ex  5351  pp0ex  5353  ord3ex  5354  abexssex  8009  mptmpoopabbrd  8122  fnpm  8885  canth2  9180  dffi3  9453  r1sucg  9806  r1pwALT  9890  rankuni  9909  rankc2  9918  rankxpu  9923  rankmapu  9925  rankxplim  9926  setrec2fun  10003  r0weon  10121  aceq3lem  10229  dfac5lem4  10235  dfac2a  10238  dfac2b  10239  pwdju1  10299  ackbij2lem2  10347  ackbij2lem3  10348  fin23lem17  10446  domtriomlem  10550  axdc2lem  10556  axdc3lem  10558  axdclem2  10628  alephsucpw  10685  canthp1lem1  10767  gchac  10796  gruina  10933  npex  11101  nrex1  11179  pnfex  11392  mnfxr  11396  ixxex  13517  prdsvallem  17657  prdsds  17667  prdshom  17670  ismre  17792  fnmre  17793  fnmrc  17813  mrcfval  17814  mrisval  17836  wunfunc  18108  catcfuccl  18325  catcxpccl  18413  lubfval  18554  glbfval  18567  issubmgm  18923  issubm  19030  issubg  19368  cntzfval  19567  sylow1lem2  19846  lsmfval  19885  pj1fval  19941  issubrng  20832  issubrg  20856  rgspnval  20897  lssset  21241  lspfval  21281  islbs  21384  lbsext  21474  lbsexg  21475  sraval  21483  ocvfval  22005  cssval  22021  isobs  22059  islinds  22148  aspval  22213  istopon  23263  dmtopon  23274  fncld  23373  leordtval2  23563  cnpfval  23585  iscnp2  23590  kgenf  23893  xkoopn  23941  xkouni  23951  dfac14  23970  xkoccn  23971  prdstopn  23980  xkoco1cn  24009  xkoco2cn  24010  xkococn  24012  xkoinjcn  24039  isfbas  24181  uzrest  24249  acufl  24269  alexsubALTlem2  24400  tsmsval2  24482  ustfn  24554  ustn0  24573  ishtpy  25326  vitali  25967  sspval  31358  shex  31847  hsupval  31969  fpwrelmap  33398  fpwrelmapffs  33399  dmvlsiga  34844  eulerpartlem1  35082  eulerpartgbij  35087  eulerpartlemmf  35090  coinflippv  35199  ballotlemoex  35201  reprval  35322  kur14lem9  36159  satfvsuclem1  36304  mpstval  36480  mclsrcl  36506  mclsval  36508  heibor1lem  38946  heibor  38958  idlval  39150  psubspset  41004  paddfval  41057  pclfvalN  41149  polfvalN  41164  psubclsetN  41196  docafvalN  42382  djafvalN  42394  dicval  42436  dochfval  42610  djhfval  42657  islpolN  42743  mzpclval  43940  eldiophb  43972  rpnnen3  44243  dfac11  44268  clsk1independent  45249  permaxpow  46205  dmvolsal  47571  ovnval  47766  smfresal  48013  sprbisymrel  48796  grtri  49253  uspgrex  49463  uspgrbisymrelALT  49468  lincop  49735  parcatid  50979  elpglem3  51096