Theorem pweq 4013

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 3526	. . 3 |- ( A = B -> ( x C_ A <-> x C_ B ) )
2	1	abbidv 2603	. 2 |- ( A = B -> { x | x C_ A } = { x | x C_ B } )
3		df-pw 4012	. 2 |- ~P A = { x | x C_ A }
4		df-pw 4012	. 2 |- ~P B = { x | x C_ B }
5	2, 3, 4	3eqtr4g 2533	1 |- ( A = B -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1379   {cab 2452   C_ wss 3476   ~Pcpw 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-pw 4012

This theorem is referenced by:  pweqi  4014  pweqd  4015  axpweq  4624  pwex  4630  pwexg  4631  pwssun  4786  knatar  6241  pwdom  7669  canth2g  7671  pwfi  7815  fival  7872  marypha1lem  7893  marypha1  7894  wdompwdom  8004  canthwdom  8005  r1sucg  8187  ranklim  8262  r1pwOLD  8264  isacn  8425  dfac12r  8526  dfac12k  8527  pwsdompw  8584  ackbij1lem5  8604  ackbij1lem8  8607  ackbij1lem14  8613  r1om  8624  fictb  8625  isfin1a  8672  isfin2  8674  isfin3  8676  isfin3ds  8709  isf33lem  8746  domtriomlem  8822  ttukeylem1  8889  elgch  9000  wunpw  9085  wunex2  9116  wuncval2  9125  eltskg  9128  eltsk2g  9129  tskpwss  9130  tskpw  9131  inar1  9153  grupw  9173  grothpw  9204  grothpwex  9205  axgroth6  9206  grothomex  9207  grothac  9208  axdc4uz  12061  hashpw  12460  hashbc  12468  ackbijnn  13603  incexclem  13611  rami  14392  ismre  14845  isacs  14906  isacs2  14908  acsfiel  14909  isacs1i  14912  mreacs  14913  isssc  15050  acsficl  15658  pmtrfval  16281  istopg  19199  istopon  19221  eltg  19253  tgdom  19274  ntrval  19331  nrmsep3  19650  iscmp  19682  cmpcov  19683  cmpsublem  19693  cmpsub  19694  tgcmp  19695  uncmp  19697  hauscmplem  19700  bwthOLD  19705  is1stc  19736  2ndc1stc  19746  llyi  19769  nllyi  19770  cldllycmp  19790  isfbas  20093  isfil  20111  filss  20117  fgval  20134  elfg  20135  isufil  20167  alexsublem  20307  alexsubb  20309  alexsubALTlem1  20310  alexsubALTlem2  20311  alexsubALTlem4  20313  alexsubALT  20314  restmetu  20853  bndth  21221  ovolicc2  21696  isuhgra  24002  isushgra  24005  uhgrac  24009  uhgraeq12d  24011  isausgra  24058  usgraeq12d  24066  ex-pw  24855  issubgo  25009  indv  27694  sigaval  27778  issiga  27779  isrnsigaOLD  27780  isrnsiga  27781  issgon  27791  measval  27837  isrnmeas  27839  rankpwg  29431  limsucncmpi  29515  neibastop1  29808  neibastop2lem  29809  neibastop2  29810  neibastop3  29811  neifg  29820  cover2g  29836  isnacs  30268  mrefg2  30271  aomclem8  30639  islssfg2  30649  lnr2i  30697  stoweidlem50  31378  stoweidlem57  31385  uhgeq12g  31865  uhguhgra  31867  uhgrauhg  31868  uhg0v  31872  isfusgra  31919  bj-snglex  33630