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

Theorem pweq 3628
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 3200 . . 3  |-  ( A  =  B  ->  (
x  C_  A  <->  x  C_  B
) )
21abbidv 2397 . 2  |-  ( A  =  B  ->  { x  |  x  C_  A }  =  { x  |  x 
C_  B } )
3 df-pw 3627 . 2  |-  ~P A  =  { x  |  x 
C_  A }
4 df-pw 3627 . 2  |-  ~P B  =  { x  |  x 
C_  B }
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  ~P A  =  ~P B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {cab 2269    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  pweqi  3629  pweqd  3630  axpweq  4187  pwex  4193  pwexg  4194  pwssun  4299  knatar  5857  pwdom  7013  canth2g  7015  pwfi  7151  fival  7166  marypha1lem  7186  marypha1  7187  wdompwdom  7292  canthwdom  7293  r1sucg  7441  ranklim  7516  r1pwOLD  7518  isacn  7671  dfac12r  7772  dfac12k  7773  pwsdompw  7830  ackbij1lem5  7850  ackbij1lem8  7853  ackbij1lem14  7859  r1om  7870  fictb  7871  isfin1a  7918  isfin2  7920  isfin3  7922  isfin3ds  7955  isf33lem  7992  domtriomlem  8068  ttukeylem1  8136  elgch  8244  wunpw  8329  wunex2  8360  wuncval2  8369  eltskg  8372  eltsk2g  8373  tskpwss  8374  tskpw  8375  inar1  8397  grupw  8417  grothpw  8448  grothpwex  8449  axgroth6  8450  grothomex  8451  grothac  8452  axdc4uz  11045  hashpw  11388  hashbc  11391  ackbijnn  12286  incexclem  12295  rami  13062  ismre  13492  isacs  13553  isacs2  13555  acsfiel  13556  isacs1i  13559  mreacs  13560  isssc  13697  acsficl  14274  istopg  16641  istopon  16663  eltg  16695  tgdom  16716  ntrval  16773  nrmsep3  17083  iscmp  17115  cmpcov  17116  cmpsublem  17126  cmpsub  17127  tgcmp  17128  uncmp  17130  hauscmplem  17133  is1stc  17167  2ndc1stc  17177  llyi  17200  nllyi  17201  cldllycmp  17221  isfbas  17524  isfil  17542  filss  17548  fgval  17565  elfg  17566  isufil  17598  alexsublem  17738  alexsubb  17740  alexsubALTlem1  17741  alexsubALTlem2  17742  alexsubALTlem4  17744  alexsubALT  17745  bndth  18456  ovolicc2  18881  ex-pw  20816  issubgo  20970  sigaval  23471  issiga  23472  isrnsigaOLD  23473  isrnsiga  23474  issgon  23484  measval  23529  isrnmeas  23531  itgmcntTMP  23588  indv  23596  rankpwg  24799  limsucncmpi  24884  imtr  25398  bwt2  25592  vtarsu  25886  partarelt1  25896  partarelt2  25897  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  neifg  26320  cover2g  26359  isnacs  26779  mrefg2  26782  aomclem8  27159  islssfg2  27169  lnr2i  27320  pmtrfval  27393  stoweidlem50  27799  stoweidlem57  27806  usgraeq12d  28111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator