Theorem pwexg 4464

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 3851	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2499	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 2965	. . 3 |- x e. _V
4	3	pwex 4463	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3019	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755   _Vcvv 2962   ~Pcpw 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-pow 4458

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850

This theorem is referenced by:  abssexg  4465  snexALT  4466  pwel  4532  uniexb  6375  xpexg  6496  fabexg  6522  undefval  6781  mapex  7208  pmvalg  7213  pw2eng  7405  fopwdom  7407  pwdom  7451  2pwne  7455  disjen  7456  domss2  7458  ssenen  7473  fineqvlem  7515  fival  7650  fipwuni  7664  hartogslem2  7745  wdompwdom  7781  harwdom  7793  tskwe  8108  ween  8193  acni  8203  acnnum  8210  infpwfien  8220  pwcda1  8351  ackbij1b  8396  fictb  8402  fin2i  8452  isfin2-2  8476  ssfin3ds  8487  fin23lem32  8501  fin23lem39  8507  fin23lem41  8509  isfin1-3  8543  fin1a2lem12  8568  canth3  8713  ondomon  8715  canthnum  8804  canthwe  8806  canthp1lem2  8808  gchxpidm  8824  gchpwdom  8825  gchhar  8834  wrdexg  12228  hashbcval  14046  restid2  14352  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  ismre  14511  isacs1i  14578  sscpwex  14711  fpwipodrs  15317  acsdrscl  15323  sylow2a  16098  opsrval  17488  istps3OLD  18369  tgdom  18425  distop  18442  fctop  18450  cctop  18452  ppttop  18453  epttop  18455  cldval  18469  ntrfval  18470  clsfval  18471  mretopd  18538  neifval  18545  neif  18546  neival  18548  neiptoptop  18577  lpfval  18584  restfpw  18625  ordtbaslem  18634  kgenval  18950  dfac14lem  19032  qtopval  19110  isfbas  19244  fbssfi  19252  fsubbas  19282  fgval  19285  filssufil  19327  hauspwpwf1  19402  hauspwpwdom  19403  flimfnfcls  19443  ptcmplem1  19466  tsmsfbas  19540  eltsms  19545  ustval  19619  isust  19620  utopval  19649  blfvalps  19800  cusgraexilem1  23197  issubgo  23613  indv  26323  sigaex  26406  sigaval  26407  pwsiga  26427  coinflipspace  26711  iscvm  26996  cvmsval  27003  altxpexg  27856  hfpw  28070  islocfin  28412  neibastop2lem  28425  fnemeet2  28432  fnejoin1  28433  elrfi  28875  elrfirn  28876  kelac2  29263