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

Theorem difeq1 3288
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 2783 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3162 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3162 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2341 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1685   {crab 2548    \ cdif 3150
This theorem is referenced by:  difeq12  3290  difeq1i  3291  difeq1d  3294  uneqdifeq  3543  hartogslem1  7253  kmlem9  7780  kmlem11  7782  kmlem12  7783  isfin1a  7914  fin1a2lem13  8034  incexclem  12291  ismri  13529  ablfac1eulem  15303  islbs  15825  lbsextlem1  15907  lbsextlem2  15908  lbsextlem3  15909  lbsextlem4  15910  lpval  16867  2ndcdisj  17178  isufil  17594  ptcmplem2  17743  mblsplit  18887  voliunlem3  18905  ig1pval  19554  ballotlemgval  23078  cvmscbv  23196  cvmsi  23203  cvmsval  23204  symdifeq1  23775  sssu  24552  bwt2  25003  f1otrspeq  26801  pmtrval  26805  pmtrfrn  26811  symgsssg  26819  symgfisg  26820  symggen  26822  psgnunilem1  26827  psgnunilem5  26828  psgneldm  26837  sdrgacs  26920  compne  27053
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-dif 3156
  Copyright terms: Public domain W3C validator