MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pweq Structured version   Unicode version

Theorem pweq 3802
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.
StepHypRef Expression
1 sseq2 3370 . . 3  |-  ( A  =  B  ->  (
x  C_  A  <->  x  C_  B
) )
21abbidv 2550 . 2  |-  ( A  =  B  ->  { x  |  x  C_  A }  =  { x  |  x 
C_  B } )
3 df-pw 3801 . 2  |-  ~P A  =  { x  |  x 
C_  A }
4 df-pw 3801 . 2  |-  ~P B  =  { x  |  x 
C_  B }
52, 3, 43eqtr4g 2493 1  |-  ( A  =  B  ->  ~P A  =  ~P B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   {cab 2422    C_ wss 3320   ~Pcpw 3799
This theorem is referenced by:  pweqi  3803  pweqd  3804  axpweq  4376  pwex  4382  pwexg  4383  pwssun  4489  knatar  6080  pwdom  7259  canth2g  7261  pwfi  7402  fival  7417  marypha1lem  7438  marypha1  7439  wdompwdom  7546  canthwdom  7547  r1sucg  7695  ranklim  7770  r1pwOLD  7772  isacn  7925  dfac12r  8026  dfac12k  8027  pwsdompw  8084  ackbij1lem5  8104  ackbij1lem8  8107  ackbij1lem14  8113  r1om  8124  fictb  8125  isfin1a  8172  isfin2  8174  isfin3  8176  isfin3ds  8209  isf33lem  8246  domtriomlem  8322  ttukeylem1  8389  elgch  8497  wunpw  8582  wunex2  8613  wuncval2  8622  eltskg  8625  eltsk2g  8626  tskpwss  8627  tskpw  8628  inar1  8650  grupw  8670  grothpw  8701  grothpwex  8702  axgroth6  8703  grothomex  8704  grothac  8705  axdc4uz  11322  hashpw  11699  hashbc  11702  ackbijnn  12607  incexclem  12616  rami  13383  ismre  13815  isacs  13876  isacs2  13878  acsfiel  13879  isacs1i  13882  mreacs  13883  isssc  14020  acsficl  14597  istopg  16968  istopon  16990  eltg  17022  tgdom  17043  ntrval  17100  nrmsep3  17419  iscmp  17451  cmpcov  17452  cmpsublem  17462  cmpsub  17463  tgcmp  17464  uncmp  17466  hauscmplem  17469  bwth  17473  is1stc  17504  2ndc1stc  17514  llyi  17537  nllyi  17538  cldllycmp  17558  isfbas  17861  isfil  17879  filss  17885  fgval  17902  elfg  17903  isufil  17935  alexsublem  18075  alexsubb  18077  alexsubALTlem1  18078  alexsubALTlem2  18079  alexsubALTlem4  18081  alexsubALT  18082  restmetu  18617  bndth  18983  ovolicc2  19418  isuhgra  21338  uhgraeq12d  21342  isausgra  21379  usgraeq12d  21385  ex-pw  21737  issubgo  21891  indv  24410  sigaval  24493  issiga  24494  isrnsigaOLD  24495  isrnsiga  24496  issgon  24506  measval  24552  isrnmeas  24554  rankpwg  26110  limsucncmpi  26195  neibastop1  26388  neibastop2lem  26389  neibastop2  26390  neibastop3  26391  neifg  26400  cover2g  26416  isnacs  26758  mrefg2  26761  aomclem8  27136  islssfg2  27146  lnr2i  27297  pmtrfval  27370  stoweidlem50  27775  stoweidlem57  27782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334  df-pw 3801
  Copyright terms: Public domain W3C validator