Theorem pwex 5345

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  𝒫 cpw 4557

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 2732  ax-sep 5251  ax-pow 5330

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559

This theorem is used by:  p0ex  5349  pp0ex  5351  ord3ex  5352  abexssex  7967  mptmpoopabbrd  8080  fnpm  8833  canth2  9128  dffi3  9401  r1sucg  9751  r1pwALT  9828  rankuni  9845  rankc2  9853  rankxpu  9858  rankmapu  9860  rankxplim  9861  r0weon  10015  aceq3lem  10123  dfac5lem4  10129  dfac2a  10132  dfac2b  10133  pwdju1  10193  ackbij2lem2  10241  ackbij2lem3  10242  fin23lem17  10340  domtriomlem  10444  axdc2lem  10450  axdc3lem  10452  axdclem2  10522  alephsucpw  10579  canthp1lem1  10661  gchac  10690  gruina  10827  npex  10995  nrex1  11073  pnfex  11286  mnfxr  11290  ixxex  13409  prdsvallem  17539  prdsds  17549  prdshom  17552  ismre  17674  fnmre  17675  fnmrc  17695  mrcfval  17696  mrisval  17718  wunfunc  17990  catcfuccl  18207  catcxpccl  18295  lubfval  18436  glbfval  18449  issubmgm  18804  issubm  18911  issubg  19249  cntzfval  19447  sylow1lem2  19726  lsmfval  19765  pj1fval  19821  issubrng  20709  issubrg  20733  rgspnval  20774  lssset  21117  lspfval  21157  islbs  21260  lbsext  21350  lbsexg  21351  sraval  21359  ocvfval  21879  cssval  21895  isobs  21933  islinds  22022  aspval  22087  istopon  23137  dmtopon  23148  fncld  23247  leordtval2  23437  cnpfval  23459  iscnp2  23464  kgenf  23767  xkoopn  23815  xkouni  23825  dfac14  23844  xkoccn  23845  prdstopn  23854  xkoco1cn  23883  xkoco2cn  23884  xkococn  23886  xkoinjcn  23913  isfbas  24055  uzrest  24123  acufl  24143  alexsubALTlem2  24274  tsmsval2  24356  ustfn  24428  ustn0  24447  ishtpy  25200  vitali  25841  sspval  31204  shex  31693  hsupval  31815  fpwrelmap  33204  fpwrelmapffs  33205  dmvlsiga  34639  eulerpartlem1  34878  eulerpartgbij  34883  eulerpartlemmf  34886  coinflippv  34995  ballotlemoex  34997  reprval  35118  kur14lem9  35793  satfvsuclem1  35938  mpstval  36114  mclsrcl  36140  mclsval  36142  heibor1lem  38559  heibor  38571  idlval  38763  psubspset  40617  paddfval  40670  pclfvalN  40762  polfvalN  40777  psubclsetN  40809  docafvalN  41995  djafvalN  42007  dicval  42049  dochfval  42223  djhfval  42270  islpolN  42356  mzpclval  43570  eldiophb  43602  rpnnen3  43873  dfac11  43903  clsk1independent  44886  permaxpow  45832  dmvolsal  47174  ovnval  47369  smfresal  47616  sprbisymrel  48399  grtri  48856  uspgrex  49066  uspgrbisymrelALT  49071  lincop  49338  setrec2fun  50618  elpglem3  50639