Theorem pwexg 4587

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 3954	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2513	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 3048	. . 3 |- x e. _V
4	3	pwex 4586	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3107	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1444   e. wcel 1887   _Vcvv 3045   ~Pcpw 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-pow 4581

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953

This theorem is referenced by:  abssexg  4588  snexALT  4589  pwel  4652  xpexg  6593  uniexb  6601  fabexg  6749  undefval  7023  mapex  7478  pmvalg  7483  pw2eng  7678  fopwdom  7680  pwdom  7724  2pwne  7728  disjen  7729  domss2  7731  ssenen  7746  fineqvlem  7786  fival  7926  fipwuni  7940  hartogslem2  8058  wdompwdom  8093  harwdom  8105  tskwe  8384  ween  8466  acni  8476  acnnum  8483  infpwfien  8493  pwcda1  8624  ackbij1b  8669  fictb  8675  fin2i  8725  isfin2-2  8749  ssfin3ds  8760  fin23lem32  8774  fin23lem39  8780  fin23lem41  8782  isfin1-3  8816  fin1a2lem12  8841  canth3  8986  ondomon  8988  canthnum  9074  canthwe  9076  canthp1lem2  9078  gchxpidm  9094  gchpwdom  9095  gchhar  9104  wrdexg  12682  hashbcval  14954  restid2  15329  prdsplusg  15356  prdsmulr  15357  prdsvsca  15358  ismre  15496  isacs1i  15563  sscpwex  15720  fpwipodrs  16410  acsdrscl  16416  sylow2a  17271  opsrval  18698  tgdom  19994  distop  20011  fctop  20019  cctop  20021  ppttop  20022  epttop  20024  cldval  20038  ntrfval  20039  clsfval  20040  mretopd  20108  neifval  20115  neif  20116  neival  20118  neiptoptop  20147  lpfval  20154  restfpw  20195  ordtbaslem  20204  islocfin  20532  dissnref  20543  kgenval  20550  dfac14lem  20632  qtopval  20710  isfbas  20844  fbssfi  20852  fsubbas  20882  fgval  20885  filssufil  20927  hauspwpwf1  21002  hauspwpwdom  21003  flimfnfcls  21043  ptcmplem1  21067  tsmsfbas  21142  eltsms  21147  ustval  21217  isust  21218  utopval  21247  blfvalps  21398  cusgraexilem1  25194  issubgo  26031  indv  28834  sigaex  28931  sigaval  28932  pwsiga  28952  pwldsys  28979  ldgenpisyslem1  28985  omsval  29117  omsvalOLD  29121  carsgval  29135  coinflipspace  29313  iscvm  29982  cvmsval  29989  altxpexg  30745  hfpw  30952  neibastop2lem  31016  fnemeet2  31023  fnejoin1  31024  elrfi  35536  elrfirn  35537  kelac2  35923  pwsal  38176  salexct  38193  psmeasurelem  38308  caragenval  38314  omeunile  38326  0ome  38350  isomennd  38352  usgrexi  39506