Theorem pweq 4002

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 3511	. . 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 4001	. 2 |- ~P A = { x | x C_ A }
4		df-pw 4001	. 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 1398   {cab 2439   C_ wss 3461   ~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-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

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-in 3468  df-ss 3475  df-pw 4001

This theorem is referenced by:  pweqi  4003  pweqd  4004  axpweq  4614  pwex  4620  pwexg  4621  pwssun  4775  knatar  6228  pwdom  7662  canth2g  7664  pwfi  7807  fival  7864  marypha1lem  7885  marypha1  7886  wdompwdom  7996  canthwdom  7997  r1sucg  8178  ranklim  8253  r1pwALT  8255  isacn  8416  dfac12r  8517  dfac12k  8518  pwsdompw  8575  ackbij1lem5  8595  ackbij1lem8  8598  ackbij1lem14  8604  r1om  8615  fictb  8616  isfin1a  8663  isfin2  8665  isfin3  8667  isfin3ds  8700  isf33lem  8737  domtriomlem  8813  ttukeylem1  8880  elgch  8989  wunpw  9074  wunex2  9105  wuncval2  9114  eltskg  9117  eltsk2g  9118  tskpwss  9119  tskpw  9120  inar1  9142  grupw  9162  grothpw  9193  grothpwex  9194  axgroth6  9195  grothomex  9196  grothac  9197  axdc4uz  12075  hashpw  12478  hashbc  12486  ackbijnn  13722  incexclem  13730  rami  14617  ismre  15079  isacs  15140  isacs2  15142  acsfiel  15143  isacs1i  15146  mreacs  15147  isssc  15308  acsficl  16000  pmtrfval  16674  istopg  19571  istopon  19593  eltg  19625  tgdom  19647  ntrval  19704  nrmsep3  20023  iscmp  20055  cmpcov  20056  cmpsublem  20066  cmpsub  20067  tgcmp  20068  uncmp  20070  hauscmplem  20073  is1stc  20108  2ndc1stc  20118  llyi  20141  nllyi  20142  cldllycmp  20162  isfbas  20496  isfil  20514  filss  20520  fgval  20537  elfg  20538  isufil  20570  alexsublem  20710  alexsubb  20712  alexsubALTlem1  20713  alexsubALTlem2  20714  alexsubALTlem4  20716  alexsubALT  20717  restmetu  21256  bndth  21624  ovolicc2  22099  isuhgra  24500  isushgra  24503  uhgrac  24507  uhgraeq12d  24509  isausgra  24556  usgraeq12d  24564  ex-pw  25352  issubgo  25503  iscref  28082  indv  28242  sigaval  28340  issiga  28341  isrnsigaOLD  28342  isrnsiga  28343  issgon  28353  isldsys  28385  measval  28406  isrnmeas  28408  rankpwg  30054  limsucncmpi  30138  neibastop1  30417  neibastop2lem  30418  neibastop2  30419  neibastop3  30420  neifg  30429  cover2g  30445  isnacs  30876  mrefg2  30879  aomclem8  31246  islssfg2  31256  lnr2i  31306  stoweidlem50  32071  stoweidlem57  32078  uhgeq12g  32742  uhguhgra  32744  uhgrauhg  32745  uhg0v  32749  isfusgra  32796  bj-snglex  34932  pwelg  38158