Theorem pwex 5317

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  p0ex  5321  pp0ex  5323  ord3ex  5324  abexssex  7916  mptmpoopabbrd  8026  fnpm  8774  canth2  9061  dffi3  9337  r1sucg  9684  r1pwALT  9761  rankuni  9778  rankc2  9786  rankxpu  9791  rankmapu  9793  rankxplim  9794  r0weon  9925  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2a  10043  dfac2b  10044  pwdju1  10104  ackbij2lem2  10152  ackbij2lem3  10153  fin23lem17  10251  domtriomlem  10355  axdc2lem  10361  axdc3lem  10363  axdclem2  10433  alephsucpw  10484  canthp1lem1  10566  gchac  10595  gruina  10732  npex  10900  nrex1  10978  pnfex  11189  mnfxr  11193  ixxex  13300  prdsvallem  17408  prdsds  17418  prdshom  17421  ismre  17543  fnmre  17544  fnmrc  17564  mrcfval  17565  mrisval  17587  wunfunc  17859  catcfuccl  18076  catcxpccl  18164  lubfval  18305  glbfval  18318  issubmgm  18661  issubm  18762  issubg  19093  cntzfval  19286  sylow1lem2  19565  lsmfval  19604  pj1fval  19660  issubrng  20515  issubrg  20539  rgspnval  20580  lssset  20919  lspfval  20959  islbs  21063  lbsext  21153  lbsexg  21154  sraval  21162  ocvfval  21656  cssval  21672  isobs  21710  islinds  21799  aspval  21862  istopon  22887  dmtopon  22898  fncld  22997  leordtval2  23187  cnpfval  23209  iscnp2  23214  kgenf  23516  xkoopn  23564  xkouni  23574  dfac14  23593  xkoccn  23594  prdstopn  23603  xkoco1cn  23632  xkoco2cn  23633  xkococn  23635  xkoinjcn  23662  isfbas  23804  uzrest  23872  acufl  23892  alexsubALTlem2  24023  tsmsval2  24105  ustfn  24177  ustn0  24196  ishtpy  24949  vitali  25590  madefi  27919  sspval  30809  shex  31298  hsupval  31420  fpwrelmap  32821  fpwrelmapffs  32822  dmvlsiga  34289  eulerpartlem1  34527  eulerpartgbij  34532  eulerpartlemmf  34535  coinflippv  34644  ballotlemoex  34646  reprval  34770  kur14lem9  35412  satfvsuclem1  35557  mpstval  35733  mclsrcl  35759  mclsval  35761  heibor1lem  38144  heibor  38156  idlval  38348  psubspset  40204  paddfval  40257  pclfvalN  40349  polfvalN  40364  psubclsetN  40396  docafvalN  41582  djafvalN  41594  dicval  41636  dochfval  41810  djhfval  41857  islpolN  41943  mzpclval  43171  eldiophb  43203  rpnnen3  43478  dfac11  43508  clsk1independent  44491  permaxpow  45454  dmvolsal  46792  ovnval  46987  smfresal  47234  sprbisymrel  47971  grtri  48428  uspgrex  48638  uspgrbisymrelALT  48643  lincop  48896  setrec2fun  50179  elpglem3  50200