Theorem pweq 3851

Description: Equality theorem for power class. (Contributed by NM, 5-Aug-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 3366	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2547	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 3850	. 2 |- ~P A = { x | x C_ A }
4		df-pw 3850	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2490	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1362   {cab 2419   C_ wss 3316   ~Pcpw 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330  df-pw 3850

This theorem is referenced by:  pweqi  3852  pweqd  3853  axpweq  4457  pwex  4463  pwexg  4464  pwssun  4614  knatar  6035  pwdom  7451  canth2g  7453  pwfi  7594  fival  7650  marypha1lem  7671  marypha1  7672  wdompwdom  7781  canthwdom  7782  r1sucg  7964  ranklim  8039  r1pwOLD  8041  isacn  8202  dfac12r  8303  dfac12k  8304  pwsdompw  8361  ackbij1lem5  8381  ackbij1lem8  8384  ackbij1lem14  8390  r1om  8401  fictb  8402  isfin1a  8449  isfin2  8451  isfin3  8453  isfin3ds  8486  isf33lem  8523  domtriomlem  8599  ttukeylem1  8666  elgch  8777  wunpw  8862  wunex2  8893  wuncval2  8902  eltskg  8905  eltsk2g  8906  tskpwss  8907  tskpw  8908  inar1  8930  grupw  8950  grothpw  8981  grothpwex  8982  axgroth6  8983  grothomex  8984  grothac  8985  axdc4uz  11789  hashpw  12182  hashbc  12190  ackbijnn  13274  incexclem  13282  rami  14059  ismre  14511  isacs  14572  isacs2  14574  acsfiel  14575  isacs1i  14578  mreacs  14579  isssc  14716  acsficl  15324  pmtrfval  15936  istopg  18350  istopon  18372  eltg  18404  tgdom  18425  ntrval  18482  nrmsep3  18801  iscmp  18833  cmpcov  18834  cmpsublem  18844  cmpsub  18845  tgcmp  18846  uncmp  18848  hauscmplem  18851  bwthOLD  18856  is1stc  18887  2ndc1stc  18897  llyi  18920  nllyi  18921  cldllycmp  18941  isfbas  19244  isfil  19262  filss  19268  fgval  19285  elfg  19286  isufil  19318  alexsublem  19458  alexsubb  19460  alexsubALTlem1  19461  alexsubALTlem2  19462  alexsubALTlem4  19464  alexsubALT  19465  restmetu  20004  bndth  20372  ovolicc2  20847  isuhgra  23060  uhgraeq12d  23064  isausgra  23101  usgraeq12d  23107  ex-pw  23459  issubgo  23613  indv  26323  sigaval  26407  issiga  26408  isrnsigaOLD  26409  isrnsiga  26410  issgon  26420  measval  26466  isrnmeas  26468  rankpwg  28054  limsucncmpi  28139  neibastop1  28424  neibastop2lem  28425  neibastop2  28426  neibastop3  28427  neifg  28436  cover2g  28452  isnacs  28885  mrefg2  28888  aomclem8  29259  islssfg2  29269  lnr2i  29317  stoweidlem50  29691  stoweidlem57  29698  bj-snglex  32070