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

Theorem difeq1 3262
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 2757 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3136 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3136 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2315 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 2522    \ cdif 3124
This theorem is referenced by:  difeq12  3264  difeq1i  3265  difeq1d  3268  uneqdifeq  3517  hartogslem1  7225  kmlem9  7752  kmlem11  7754  kmlem12  7755  isfin1a  7886  fin1a2lem13  8006  ismri  13496  ablfac1eulem  15270  islbs  15792  lbsextlem1  15874  lbsextlem2  15875  lbsextlem3  15876  lbsextlem4  15877  lpval  16834  2ndcdisj  17145  isufil  17561  ptcmplem2  17710  mblsplit  18854  voliunlem3  18872  ig1pval  19521  ballotlemgval  23044  cvmscbv  23162  cvmsi  23169  cvmsval  23170  symdifeq1  23741  sssu  24509  bwt2  24960  f1otrspeq  26758  pmtrval  26762  pmtrfrn  26768  symgsssg  26776  symgfisg  26777  symggen  26779  psgnunilem1  26784  psgnunilem5  26785  psgneldm  26794  sdrgacs  26877  compne  27011
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rab 2527  df-dif 3130
  Copyright terms: Public domain W3C validator