Theorem pweq 3984

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 3486	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2553	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 3983	. 2 |- ~P A = { x | x C_ A }
4		df-pw 3983	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2488	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1437   {cab 2407   C_ wss 3436   ~Pcpw 3981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-pw 3983

This theorem is referenced by:  pweqi  3985  pweqd  3986  axpweq  4601  pwex  4607  pwexg  4608  pwssun  4759  knatar  6263  pwdom  7733  canth2g  7735  pwfi  7878  fival  7935  marypha1lem  7956  marypha1  7957  wdompwdom  8102  canthwdom  8103  r1sucg  8248  ranklim  8323  r1pwALT  8325  isacn  8482  dfac12r  8583  dfac12k  8584  pwsdompw  8641  ackbij1lem5  8661  ackbij1lem8  8664  ackbij1lem14  8670  r1om  8681  fictb  8682  isfin1a  8729  isfin2  8731  isfin3  8733  isfin3ds  8766  isf33lem  8803  domtriomlem  8879  ttukeylem1  8946  elgch  9054  wunpw  9139  wunex2  9170  wuncval2  9179  eltskg  9182  eltsk2g  9183  tskpwss  9184  tskpw  9185  inar1  9207  grupw  9227  grothpw  9258  grothpwex  9259  axgroth6  9260  grothomex  9261  grothac  9262  axdc4uz  12202  hashpw  12612  hashbc  12620  ackbijnn  13885  incexclem  13893  rami  14971  ismre  15495  isacs  15556  isacs2  15558  acsfiel  15559  isacs1i  15562  mreacs  15563  isssc  15724  acsficl  16416  pmtrfval  17090  istopg  19923  istopon  19938  eltg  19970  tgdom  19992  ntrval  20049  nrmsep3  20369  iscmp  20401  cmpcov  20402  cmpsublem  20412  cmpsub  20413  tgcmp  20414  uncmp  20416  hauscmplem  20419  is1stc  20454  2ndc1stc  20464  llyi  20487  nllyi  20488  cldllycmp  20508  isfbas  20842  isfil  20860  filss  20866  fgval  20883  elfg  20884  isufil  20916  alexsublem  21057  alexsubb  21059  alexsubALTlem1  21060  alexsubALTlem2  21061  alexsubALTlem4  21063  alexsubALT  21064  restmetu  21583  bndth  21984  ovolicc2  22474  isuhgra  25023  isushgra  25026  uhgrac  25030  uhgraeq12d  25032  isausgra  25079  usgraeq12d  25087  ex-pw  25877  issubgo  26029  iscref  28679  indv  28842  sigaval  28940  issiga  28941  isrnsigaOLD  28942  isrnsiga  28943  issgon  28953  isldsys  28986  issros  29005  measval  29028  isrnmeas  29030  rankpwg  30941  neibastop1  31020  neibastop2lem  31021  neibastop2  31022  neibastop3  31023  neifg  31032  limsucncmpi  31110  bj-snglex  31535  cover2g  32005  isnacs  35515  mrefg2  35518  aomclem8  35889  islssfg2  35899  lnr2i  35945  pwelg  36134  stoweidlem50  37851  stoweidlem57  37858  issal  38096  omessle  38227  uhgreq12g  38987  uhgruhgra  38989  uhgrauhgr  38990  uhgr0v  38994  isumgr  39003  isuspgr  39032  isusgr  39033  usgrop  39044  isausgr  39045  usgr1vr  39105  usgrexmpl  39111  nbuhgr2vtx1edgblem  39183  uhgeq12gALTV  39301  uhguhgra  39303  uhgrauhg  39304  uhg0v  39308  isfusgra  39355