Theorem pwex 5341

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558

This theorem is used by:  p0ex  5345  pp0ex  5347  ord3ex  5348  abexssex  7982  mptmpoopabbrd  8094  fnpm  8857  canth2  9152  dffi3  9426  r1sucg  9779  r1pwALT  9863  rankuni  9882  rankc2  9891  rankxpu  9896  rankmapu  9898  rankxplim  9899  setrec2fun  9976  r0weon  10094  aceq3lem  10202  dfac5lem4  10208  dfac2a  10211  dfac2b  10212  pwdju1  10272  ackbij2lem2  10320  ackbij2lem3  10321  fin23lem17  10419  domtriomlem  10523  axdc2lem  10529  axdc3lem  10531  axdclem2  10601  alephsucpw  10658  canthp1lem1  10740  gchac  10769  gruina  10906  npex  11074  nrex1  11152  pnfex  11365  mnfxr  11369  ixxex  13490  prdsvallem  17630  prdsds  17640  prdshom  17643  ismre  17765  fnmre  17766  fnmrc  17786  mrcfval  17787  mrisval  17809  wunfunc  18081  catcfuccl  18298  catcxpccl  18386  lubfval  18527  glbfval  18540  issubmgm  18896  issubm  19003  issubg  19341  cntzfval  19539  sylow1lem2  19818  lsmfval  19857  pj1fval  19913  issubrng  20804  issubrg  20828  rgspnval  20869  lssset  21213  lspfval  21253  islbs  21356  lbsext  21446  lbsexg  21447  sraval  21455  ocvfval  21977  cssval  21993  isobs  22031  islinds  22120  aspval  22185  istopon  23235  dmtopon  23246  fncld  23345  leordtval2  23535  cnpfval  23557  iscnp2  23562  kgenf  23865  xkoopn  23913  xkouni  23923  dfac14  23942  xkoccn  23943  prdstopn  23952  xkoco1cn  23981  xkoco2cn  23982  xkococn  23984  xkoinjcn  24011  isfbas  24153  uzrest  24221  acufl  24241  alexsubALTlem2  24372  tsmsval2  24454  ustfn  24526  ustn0  24545  ishtpy  25298  vitali  25939  sspval  31330  shex  31819  hsupval  31941  fpwrelmap  33371  fpwrelmapffs  33372  dmvlsiga  34807  eulerpartlem1  35045  eulerpartgbij  35050  eulerpartlemmf  35053  coinflippv  35162  ballotlemoex  35164  reprval  35285  kur14lem9  36065  satfvsuclem1  36210  mpstval  36386  mclsrcl  36412  mclsval  36414  heibor1lem  38836  heibor  38848  idlval  39040  psubspset  40894  paddfval  40947  pclfvalN  41039  polfvalN  41054  psubclsetN  41086  docafvalN  42272  djafvalN  42284  dicval  42326  dochfval  42500  djhfval  42547  islpolN  42633  mzpclval  43829  eldiophb  43861  rpnnen3  44132  dfac11  44157  clsk1independent  45139  permaxpow  46092  dmvolsal  47449  ovnval  47644  smfresal  47891  sprbisymrel  48674  grtri  49131  uspgrex  49341  uspgrbisymrelALT  49346  lincop  49613  parcatid  50857  elpglem3  50974