Theorem pwexg 4343

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.)

Assertion

Ref	Expression
pwexg	|- ( A e. V -> ~P A e. _V )

Proof of Theorem pwexg

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pweq 3762	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2470	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 2919	. . 3 |- x e. _V
4	3	pwex 4342	. 2 |- ~P x e. _V
5	2, 4	vtoclg 2971	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721   _Vcvv 2916   ~Pcpw 3759

This theorem is referenced by:  abssexg  4344  snexALT  4345  pwel  4375  uniexb  4711  xpexg  4948  fabexg  5583  undefval  6505  mapex  6983  pmvalg  6988  pw2eng  7173  fopwdom  7175  pwdom  7218  2pwne  7222  disjen  7223  domss2  7225  ssenen  7240  fineqvlem  7282  fival  7375  fipwuni  7389  hartogslem2  7468  wdompwdom  7502  harwdom  7514  tskwe  7793  ween  7872  acni  7882  acnnum  7889  infpwfien  7899  pwcda1  8030  ackbij1b  8075  fictb  8081  fin2i  8131  isfin2-2  8155  ssfin3ds  8166  fin23lem32  8180  fin23lem39  8186  fin23lem41  8188  isfin1-3  8222  fin1a2lem12  8247  canth3  8392  ondomon  8394  canthnum  8480  canthwe  8482  canthp1lem2  8484  gchxpidm  8500  gchhar  8502  gchpwdom  8505  wrdexg  11694  hashbcval  13325  restid2  13613  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  ismre  13770  isacs1i  13837  sscpwex  13970  fpwipodrs  14545  acsdrscl  14551  sylow2a  15208  opsrval  16490  istps3OLD  16942  tgdom  16998  distop  17015  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  cldval  17042  ntrfval  17043  clsfval  17044  mretopd  17111  neifval  17118  neif  17119  neival  17121  neiptoptop  17150  lpfval  17157  restfpw  17197  ordtbaslem  17206  kgenval  17520  dfac14lem  17602  qtopval  17680  isfbas  17814  fbssfi  17822  fsubbas  17852  fgval  17855  filssufil  17897  hauspwpwf1  17972  hauspwpwdom  17973  flimfnfcls  18013  ptcmplem1  18036  tsmsfbas  18110  eltsms  18115  ustval  18185  isust  18186  utopval  18215  blfvalps  18366  cusgraexilem1  21428  issubgo  21844  indv  24363  sigaex  24445  sigaval  24446  pwsiga  24466  coinflipspace  24691  iscvm  24899  cvmsval  24906  altxpexg  25727  hfpw  26030  islocfin  26266  neibastop2lem  26279  fnemeet2  26286  fnejoin1  26287  elrfi  26638  elrfirn  26639  kelac2  27031

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-pow 4337

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761