Theorem pwex 5353

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-pw 4565

This theorem is referenced by:  p0ex  5357  pp0ex  5359  ord3ex  5360  abexssex  7968  mptmpoopabbrd  8079  fnpm  8832  canth2  9119  dffi3  9392  r1sucg  9742  r1pwALT  9819  rankuni  9836  rankc2  9844  rankxpu  9849  rankmapu  9851  rankxplim  9852  r0weon  9997  aceq3lem  10105  dfac5lem4  10111  dfac2a  10114  dfac2b  10115  pwdju1  10175  ackbij2lem2  10223  ackbij2lem3  10224  fin23lem17  10323  domtriomlem  10427  axdc2lem  10433  axdc3lem  10435  axdclem2  10505  alephsucpw  10556  canthp1lem1  10638  gchac  10667  gruina  10804  npex  10972  nrex1  11050  pnfex  11263  mnfxr  11267  ixxex  13384  prdsvallem  17508  prdsds  17518  prdshom  17521  ismre  17643  fnmre  17644  fnmrc  17664  mrcfval  17665  mrisval  17687  wunfunc  17959  catcfuccl  18176  catcxpccl  18264  lubfval  18405  glbfval  18418  issubmgm  18761  issubm  18862  issubg  19193  cntzfval  19391  sylow1lem2  19670  lsmfval  19709  pj1fval  19765  issubrng  20633  issubrg  20657  rgspnval  20698  lssset  21035  lspfval  21075  islbs  21178  lbsext  21268  lbsexg  21269  sraval  21277  ocvfval  21797  cssval  21813  isobs  21851  islinds  21940  aspval  22003  istopon  23050  dmtopon  23061  fncld  23160  leordtval2  23350  cnpfval  23372  iscnp2  23377  kgenf  23679  xkoopn  23727  xkouni  23737  dfac14  23756  xkoccn  23757  prdstopn  23766  xkoco1cn  23795  xkoco2cn  23796  xkococn  23798  xkoinjcn  23825  isfbas  23967  uzrest  24035  acufl  24055  alexsubALTlem2  24186  tsmsval2  24268  ustfn  24340  ustn0  24359  ishtpy  25112  vitali  25753  madefi  28087  sspval  31056  shex  31545  hsupval  31667  fpwrelmap  33059  fpwrelmapffs  33060  dmvlsiga  34500  eulerpartlem1  34738  eulerpartgbij  34743  eulerpartlemmf  34746  coinflippv  34855  ballotlemoex  34857  reprval  34978  kur14lem9  35687  satfvsuclem1  35832  mpstval  36008  mclsrcl  36034  mclsval  36036  heibor1lem  38441  heibor  38453  idlval  38645  psubspset  40499  paddfval  40552  pclfvalN  40644  polfvalN  40659  psubclsetN  40691  docafvalN  41877  djafvalN  41889  dicval  41931  dochfval  42105  djhfval  42152  islpolN  42238  mzpclval  43439  eldiophb  43471  rpnnen3  43742  dfac11  43772  clsk1independent  44755  permaxpow  45701  dmvolsal  47043  ovnval  47238  smfresal  47485  sprbisymrel  48231  grtri  48688  uspgrex  48898  uspgrbisymrelALT  48903  lincop  49171  setrec2fun  50453  elpglem3  50474