Theorem pweq 3970

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 3485	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2590	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 3969	. 2 |- ~P A = { x | x C_ A }
4		df-pw 3969	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2520	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1370   {cab 2439   C_ wss 3435   ~Pcpw 3967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449  df-pw 3969

This theorem is referenced by:  pweqi  3971  pweqd  3972  axpweq  4576  pwex  4582  pwexg  4583  pwssun  4734  knatar  6156  pwdom  7572  canth2g  7574  pwfi  7716  fival  7772  marypha1lem  7793  marypha1  7794  wdompwdom  7903  canthwdom  7904  r1sucg  8086  ranklim  8161  r1pwOLD  8163  isacn  8324  dfac12r  8425  dfac12k  8426  pwsdompw  8483  ackbij1lem5  8503  ackbij1lem8  8506  ackbij1lem14  8512  r1om  8523  fictb  8524  isfin1a  8571  isfin2  8573  isfin3  8575  isfin3ds  8608  isf33lem  8645  domtriomlem  8721  ttukeylem1  8788  elgch  8899  wunpw  8984  wunex2  9015  wuncval2  9024  eltskg  9027  eltsk2g  9028  tskpwss  9029  tskpw  9030  inar1  9052  grupw  9072  grothpw  9103  grothpwex  9104  axgroth6  9105  grothomex  9106  grothac  9107  axdc4uz  11921  hashpw  12315  hashbc  12323  ackbijnn  13408  incexclem  13416  rami  14193  ismre  14646  isacs  14707  isacs2  14709  acsfiel  14710  isacs1i  14713  mreacs  14714  isssc  14851  acsficl  15459  pmtrfval  16074  istopg  18639  istopon  18661  eltg  18693  tgdom  18714  ntrval  18771  nrmsep3  19090  iscmp  19122  cmpcov  19123  cmpsublem  19133  cmpsub  19134  tgcmp  19135  uncmp  19137  hauscmplem  19140  bwthOLD  19145  is1stc  19176  2ndc1stc  19186  llyi  19209  nllyi  19210  cldllycmp  19230  isfbas  19533  isfil  19551  filss  19557  fgval  19574  elfg  19575  isufil  19607  alexsublem  19747  alexsubb  19749  alexsubALTlem1  19750  alexsubALTlem2  19751  alexsubALTlem4  19753  alexsubALT  19754  restmetu  20293  bndth  20661  ovolicc2  21136  isuhgra  23388  uhgraeq12d  23392  isausgra  23429  usgraeq12d  23435  ex-pw  23787  issubgo  23941  indv  26613  sigaval  26697  issiga  26698  isrnsigaOLD  26699  isrnsiga  26700  issgon  26710  measval  26756  isrnmeas  26758  rankpwg  28350  limsucncmpi  28434  neibastop1  28727  neibastop2lem  28728  neibastop2  28729  neibastop3  28730  neifg  28739  cover2g  28755  isnacs  29187  mrefg2  29190  aomclem8  29561  islssfg2  29571  lnr2i  29619  stoweidlem50  29992  stoweidlem57  29999  bj-snglex  32783