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

Theorem difeq1 3374
Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
difeq1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )

Proof of Theorem difeq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 rabeq 2867 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3247 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3247 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2423 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1647    e. wcel 1715   {crab 2632    \ cdif 3235
This theorem is referenced by:  difeq12  3376  difeq1i  3377  difeq1d  3380  uneqdifeq  3631  hartogslem1  7404  kmlem9  7931  kmlem11  7933  kmlem12  7934  isfin1a  8065  fin1a2lem13  8185  incexclem  12503  ismri  13743  ablfac1eulem  15517  islbs  16039  lbsextlem1  16121  lbsextlem2  16122  lbsextlem3  16123  lbsextlem4  16124  lpval  17088  2ndcdisj  17399  isufil  17811  ptcmplem2  17960  mblsplit  19106  voliunlem3  19124  ig1pval  19773  difeq  23395  sigaval  23958  issiga  23959  issgon  23971  probun  24125  ballotlemgval  24229  cvmscbv  24392  cvmsi  24399  cvmsval  24400  symdifeq1  25105  f1otrspeq  26896  pmtrval  26900  pmtrfrn  26906  symgsssg  26914  symgfisg  26915  symggen  26917  psgnunilem1  26922  psgnunilem5  26923  psgneldm  26932  sdrgacs  27015  compne  27148  nb3graprlem2  27617  iscusgra  27621  isuvtx  27653  isfrgra  27825  1vwmgra  27838  3vfriswmgra  27840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-dif 3241
  Copyright terms: Public domain W3C validator