Theorem pwex 4981

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

Syntax hints:   ∈ wcel 2145  Vcvv 3351  𝒫 cpw 4297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751  ax-sep 4915  ax-pow 4974

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-in 3730  df-ss 3737  df-pw 4299

This theorem is referenced by:  p0ex  4984  pp0ex  4986  ord3ex  4987  abexssex  7296  fnpm  8017  canth2  8269  dffi3  8493  r1sucg  8796  r1pwALT  8873  rankuni  8890  rankc2  8898  rankxpu  8903  rankmapu  8905  rankxplim  8906  r0weon  9035  aceq3lem  9143  dfac5lem4  9149  dfac2a  9152  dfac2b  9153  dfac2OLD  9155  ackbij2lem2  9264  ackbij2lem3  9265  fin23lem17  9362  domtriomlem  9466  axdc2lem  9472  axdc3lem  9474  axdclem2  9544  alephsucpw  9594  canthp1lem1  9676  gchac  9705  gruina  9842  npex  10010  axcnex  10170  pnfxr  10294  mnfxr  10298  ixxex  12391  prdsval  16323  prdsds  16332  prdshom  16335  ismre  16458  fnmre  16459  fnmrc  16475  mrcfval  16476  mrisval  16498  wunfunc  16766  catcfuccl  16966  catcxpccl  17055  lubfval  17186  glbfval  17199  issubm  17555  issubg  17802  cntzfval  17960  sylow1lem2  18221  lsmfval  18260  pj1fval  18314  issubrg  18990  lssset  19144  lspfval  19186  islbs  19289  lbsext  19378  lbsexg  19379  sraval  19391  aspval  19543  ocvfval  20227  cssval  20243  isobs  20281  islinds  20365  istopon  20937  dmtopon  20948  fncld  21047  leordtval2  21237  cnpfval  21259  iscnp2  21264  kgenf  21565  xkoopn  21613  xkouni  21623  dfac14  21642  xkoccn  21643  prdstopn  21652  xkoco1cn  21681  xkoco2cn  21682  xkococn  21684  xkoinjcn  21711  isfbas  21853  uzrest  21921  acufl  21941  alexsubALTlem2  22072  tsmsval2  22153  ustfn  22225  ustn0  22244  ishtpy  22991  vitali  23601  sspval  27918  shex  28409  hsupval  28533  fpwrelmap  29848  fpwrelmapffs  29849  isrnsigaOLD  30515  dmvlsiga  30532  eulerpartlem1  30769  eulerpartgbij  30774  eulerpartlemmf  30777  coinflippv  30885  ballotlemoex  30887  reprval  31028  kur14lem9  31534  mpstval  31770  mclsrcl  31796  mclsval  31798  heibor1lem  33940  heibor  33952  idlval  34144  psubspset  35552  paddfval  35605  pclfvalN  35697  polfvalN  35712  psubclsetN  35744  docafvalN  36932  djafvalN  36944  dicval  36986  dochfval  37160  djhfval  37207  islpolN  37293  mzpclval  37814  eldiophb  37846  rpnnen3  38125  dfac11  38158  rgspnval  38264  clsk1independent  38870  dmvolsal  41081  ovnval  41275  smfresal  41515  sprbisymrel  42277  uspgrex  42286  uspgrbisymrelALT  42291  issubmgm  42317  lincop  42725  setrec2fun  42967  vsetrec  42977  elpglem3  42987