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

Theorem pweq 3641
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 3213 . . 3  |-  ( A  =  B  ->  (
x  C_  A  <->  x  C_  B
) )
21abbidv 2410 . 2  |-  ( A  =  B  ->  { x  |  x  C_  A }  =  { x  |  x 
C_  B } )
3 df-pw 3640 . 2  |-  ~P A  =  { x  |  x 
C_  A }
4 df-pw 3640 . 2  |-  ~P B  =  { x  |  x 
C_  B }
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  ~P A  =  ~P B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   {cab 2282    C_ wss 3165   ~Pcpw 3638
This theorem is referenced by:  pweqi  3642  pweqd  3643  axpweq  4203  pwex  4209  pwexg  4210  pwssun  4315  knatar  5873  pwdom  7029  canth2g  7031  pwfi  7167  fival  7182  marypha1lem  7202  marypha1  7203  wdompwdom  7308  canthwdom  7309  r1sucg  7457  ranklim  7532  r1pwOLD  7534  isacn  7687  dfac12r  7788  dfac12k  7789  pwsdompw  7846  ackbij1lem5  7866  ackbij1lem8  7869  ackbij1lem14  7875  r1om  7886  fictb  7887  isfin1a  7934  isfin2  7936  isfin3  7938  isfin3ds  7971  isf33lem  8008  domtriomlem  8084  ttukeylem1  8152  elgch  8260  wunpw  8345  wunex2  8376  wuncval2  8385  eltskg  8388  eltsk2g  8389  tskpwss  8390  tskpw  8391  inar1  8413  grupw  8433  grothpw  8464  grothpwex  8465  axgroth6  8466  grothomex  8467  grothac  8468  axdc4uz  11061  hashpw  11404  hashbc  11407  ackbijnn  12302  incexclem  12311  rami  13078  ismre  13508  isacs  13569  isacs2  13571  acsfiel  13572  isacs1i  13575  mreacs  13576  isssc  13713  acsficl  14290  istopg  16657  istopon  16679  eltg  16711  tgdom  16732  ntrval  16789  nrmsep3  17099  iscmp  17131  cmpcov  17132  cmpsublem  17142  cmpsub  17143  tgcmp  17144  uncmp  17146  hauscmplem  17149  is1stc  17183  2ndc1stc  17193  llyi  17216  nllyi  17217  cldllycmp  17237  isfbas  17540  isfil  17558  filss  17564  fgval  17581  elfg  17582  isufil  17614  alexsublem  17754  alexsubb  17756  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALTlem4  17760  alexsubALT  17761  bndth  18472  ovolicc2  18897  ex-pw  20832  issubgo  20986  sigaval  23486  issiga  23487  isrnsigaOLD  23488  isrnsiga  23489  issgon  23499  measval  23544  isrnmeas  23546  itgmcntTMP  23603  indv  23611  rankpwg  24871  limsucncmpi  24956  imtr  25501  bwt2  25695  vtarsu  25989  partarelt1  25999  partarelt2  26000  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  neibastop3  26414  neifg  26423  cover2g  26462  isnacs  26882  mrefg2  26885  aomclem8  27262  islssfg2  27272  lnr2i  27423  pmtrfval  27496  stoweidlem50  27902  stoweidlem57  27909  usgraeq12d  28245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator