Theorem pwexg 4621

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 4002	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2523	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 3109	. . 3 |- x e. _V
4	3	pwex 4620	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3164	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 1823   _Vcvv 3106   ~Pcpw 3999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-pow 4615

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108  df-in 3468  df-ss 3475  df-pw 4001

This theorem is referenced by:  abssexg  4622  snexALT  4623  pwel  4689  xpexg  6575  uniexb  6583  fabexg  6729  undefval  6997  mapex  7418  pmvalg  7423  pw2eng  7616  fopwdom  7618  pwdom  7662  2pwne  7666  disjen  7667  domss2  7669  ssenen  7684  fineqvlem  7727  fival  7864  fipwuni  7878  hartogslem2  7960  wdompwdom  7996  harwdom  8008  tskwe  8322  ween  8407  acni  8417  acnnum  8424  infpwfien  8434  pwcda1  8565  ackbij1b  8610  fictb  8616  fin2i  8666  isfin2-2  8690  ssfin3ds  8701  fin23lem32  8715  fin23lem39  8721  fin23lem41  8723  isfin1-3  8757  fin1a2lem12  8782  canth3  8927  ondomon  8929  canthnum  9016  canthwe  9018  canthp1lem2  9020  gchxpidm  9036  gchpwdom  9037  gchhar  9046  wrdexg  12544  hashbcval  14604  restid2  14920  prdsplusg  14947  prdsmulr  14948  prdsvsca  14949  ismre  15079  isacs1i  15146  sscpwex  15303  fpwipodrs  15993  acsdrscl  15999  sylow2a  16838  opsrval  18334  istps3OLD  19590  tgdom  19647  distop  19664  fctop  19672  cctop  19674  ppttop  19675  epttop  19677  cldval  19691  ntrfval  19692  clsfval  19693  mretopd  19760  neifval  19767  neif  19768  neival  19770  neiptoptop  19799  lpfval  19806  restfpw  19847  ordtbaslem  19856  islocfin  20184  dissnref  20195  kgenval  20202  dfac14lem  20284  qtopval  20362  isfbas  20496  fbssfi  20504  fsubbas  20534  fgval  20537  filssufil  20579  hauspwpwf1  20654  hauspwpwdom  20655  flimfnfcls  20695  ptcmplem1  20718  tsmsfbas  20792  eltsms  20797  ustval  20871  isust  20872  utopval  20901  blfvalps  21052  cusgraexilem1  24668  issubgo  25503  indv  28242  sigaex  28339  sigaval  28340  pwsiga  28360  omsval  28501  carsgval  28511  coinflipspace  28683  iscvm  28968  cvmsval  28975  altxpexg  29856  hfpw  30070  neibastop2lem  30418  fnemeet2  30425  fnejoin1  30426  elrfi  30866  elrfirn  30867  kelac2  31250