Theorem pweq 3988

Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
pweq	|- ( A = B -> ~P A = ~P B )

Proof of Theorem pweq

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 3492	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2565	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 3987	. 2 |- ~P A = { x | x C_ A }
4		df-pw 3987	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1437   {cab 2414   C_ wss 3442   ~Pcpw 3985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456  df-pw 3987

This theorem is referenced by:  pweqi  3989  pweqd  3990  axpweq  4602  pwex  4608  pwexg  4609  pwssun  4760  knatar  6263  pwdom  7730  canth2g  7732  pwfi  7875  fival  7932  marypha1lem  7953  marypha1  7954  wdompwdom  8093  canthwdom  8094  r1sucg  8239  ranklim  8314  r1pwALT  8316  isacn  8473  dfac12r  8574  dfac12k  8575  pwsdompw  8632  ackbij1lem5  8652  ackbij1lem8  8655  ackbij1lem14  8661  r1om  8672  fictb  8673  isfin1a  8720  isfin2  8722  isfin3  8724  isfin3ds  8757  isf33lem  8794  domtriomlem  8870  ttukeylem1  8937  elgch  9046  wunpw  9131  wunex2  9162  wuncval2  9171  eltskg  9174  eltsk2g  9175  tskpwss  9176  tskpw  9177  inar1  9199  grupw  9219  grothpw  9250  grothpwex  9251  axgroth6  9252  grothomex  9253  grothac  9254  axdc4uz  12193  hashpw  12603  hashbc  12611  ackbijnn  13864  incexclem  13872  rami  14935  ismre  15447  isacs  15508  isacs2  15510  acsfiel  15511  isacs1i  15514  mreacs  15515  isssc  15676  acsficl  16368  pmtrfval  17042  istopg  19856  istopon  19871  eltg  19903  tgdom  19925  ntrval  19982  nrmsep3  20302  iscmp  20334  cmpcov  20335  cmpsublem  20345  cmpsub  20346  tgcmp  20347  uncmp  20349  hauscmplem  20352  is1stc  20387  2ndc1stc  20397  llyi  20420  nllyi  20421  cldllycmp  20441  isfbas  20775  isfil  20793  filss  20799  fgval  20816  elfg  20817  isufil  20849  alexsublem  20990  alexsubb  20992  alexsubALTlem1  20993  alexsubALTlem2  20994  alexsubALTlem4  20996  alexsubALT  20997  restmetu  21516  bndth  21882  ovolicc2  22353  isuhgra  24871  isushgra  24874  uhgrac  24878  uhgraeq12d  24880  isausgra  24927  usgraeq12d  24935  ex-pw  25724  issubgo  25876  iscref  28510  indv  28673  sigaval  28771  issiga  28772  isrnsigaOLD  28773  isrnsiga  28774  issgon  28784  isldsys  28817  issros  28836  measval  28859  isrnmeas  28861  rankpwg  30721  neibastop1  30800  neibastop2lem  30801  neibastop2  30802  neibastop3  30803  neifg  30812  limsucncmpi  30890  bj-snglex  31316  cover2g  31745  isnacs  35255  mrefg2  35258  aomclem8  35625  islssfg2  35635  lnr2i  35681  pwelg  35863  stoweidlem50  37480  stoweidlem57  37487  issal  37722  omessle  37828  uhgeq12g  38440  uhguhgra  38442  uhgrauhg  38443  uhg0v  38447  isfusgra  38494