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

Theorem difeq1 3229
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
StepHypRef Expression
1 rabeq 2734 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3103 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3103 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2313 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    = wceq 1619    e. wcel 1621   {crab 2519    \ cdif 3091
This theorem is referenced by:  difeq12  3231  difeq1i  3232  difeq1d  3235  uneqdifeq  3484  hartogslem1  7190  kmlem9  7717  kmlem11  7719  kmlem12  7720  isfin1a  7851  fin1a2lem13  7971  ismri  13460  ablfac1eulem  15234  islbs  15756  lbsextlem1  15838  lbsextlem2  15839  lbsextlem3  15840  lbsextlem4  15841  lpval  16798  2ndcdisj  17109  isufil  17525  ptcmplem2  17674  mblsplit  18818  voliunlem3  18836  ig1pval  19485  ballotlemgval  23008  cvmscbv  23126  cvmsi  23133  cvmsval  23134  symdifeq1  23705  sssu  24473  bwt2  24924  f1otrspeq  26722  pmtrval  26726  pmtrfrn  26732  symgsssg  26740  symgfisg  26741  symggen  26743  psgnunilem1  26748  psgnunilem5  26749  psgneldm  26758  sdrgacs  26841  compne  26975
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2523  df-dif 3097
  Copyright terms: Public domain W3C validator