Theorem pwexg 4606

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 3983	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2492	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 3085	. . 3 |- x e. _V
4	3	pwex 4605	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3140	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1438   e. wcel 1869   _Vcvv 3082   ~Pcpw 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-pow 4600

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-v 3084  df-in 3444  df-ss 3451  df-pw 3982

This theorem is referenced by:  abssexg  4607  snexALT  4608  pwel  4671  xpexg  6605  uniexb  6613  fabexg  6761  undefval  7029  mapex  7484  pmvalg  7489  pw2eng  7682  fopwdom  7684  pwdom  7728  2pwne  7732  disjen  7733  domss2  7735  ssenen  7750  fineqvlem  7790  fival  7930  fipwuni  7944  hartogslem2  8062  wdompwdom  8097  harwdom  8109  tskwe  8387  ween  8468  acni  8478  acnnum  8485  infpwfien  8495  pwcda1  8626  ackbij1b  8671  fictb  8677  fin2i  8727  isfin2-2  8751  ssfin3ds  8762  fin23lem32  8776  fin23lem39  8782  fin23lem41  8784  isfin1-3  8818  fin1a2lem12  8843  canth3  8988  ondomon  8990  canthnum  9076  canthwe  9078  canthp1lem2  9080  gchxpidm  9096  gchpwdom  9097  gchhar  9106  wrdexg  12680  hashbcval  14947  restid2  15322  prdsplusg  15349  prdsmulr  15350  prdsvsca  15351  ismre  15489  isacs1i  15556  sscpwex  15713  fpwipodrs  16403  acsdrscl  16409  sylow2a  17264  opsrval  18691  tgdom  19986  distop  20003  fctop  20011  cctop  20013  ppttop  20014  epttop  20016  cldval  20030  ntrfval  20031  clsfval  20032  mretopd  20100  neifval  20107  neif  20108  neival  20110  neiptoptop  20139  lpfval  20146  restfpw  20187  ordtbaslem  20196  islocfin  20524  dissnref  20535  kgenval  20542  dfac14lem  20624  qtopval  20702  isfbas  20836  fbssfi  20844  fsubbas  20874  fgval  20877  filssufil  20919  hauspwpwf1  20994  hauspwpwdom  20995  flimfnfcls  21035  ptcmplem1  21059  tsmsfbas  21134  eltsms  21139  ustval  21209  isust  21210  utopval  21239  blfvalps  21390  cusgraexilem1  25186  issubgo  26023  indv  28836  sigaex  28933  sigaval  28934  pwsiga  28954  pwldsys  28981  ldgenpisyslem1  28987  omsval  29119  omsvalOLD  29123  carsgval  29137  coinflipspace  29315  iscvm  29984  cvmsval  29991  altxpexg  30744  hfpw  30951  neibastop2lem  31015  fnemeet2  31022  fnejoin1  31023  elrfi  35499  elrfirn  35500  kelac2  35887  pwsal  38021  psmeasurelem  38131  caragenval  38137  omeunile  38149  0ome  38173  isomennd  38175