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

Theorem difeq1 3289
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 2784 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3163 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3163 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2342 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1625    e. wcel 1686   {crab 2549    \ cdif 3151
This theorem is referenced by:  difeq12  3291  difeq1i  3292  difeq1d  3295  uneqdifeq  3544  hartogslem1  7259  kmlem9  7786  kmlem11  7788  kmlem12  7789  isfin1a  7920  fin1a2lem13  8040  incexclem  12297  ismri  13535  ablfac1eulem  15309  islbs  15831  lbsextlem1  15913  lbsextlem2  15914  lbsextlem3  15915  lbsextlem4  15916  lpval  16873  2ndcdisj  17184  isufil  17600  ptcmplem2  17749  mblsplit  18893  voliunlem3  18911  ig1pval  19560  ballotlemgval  23084  difeq  23130  sigaval  23473  issiga  23474  issgon  23486  probun  23624  cvmscbv  23791  cvmsi  23798  cvmsval  23799  symdifeq1  24366  sssu  25152  bwt2  25603  f1otrspeq  27401  pmtrval  27405  pmtrfrn  27411  symgsssg  27419  symgfisg  27420  symggen  27422  psgnunilem1  27427  psgnunilem5  27428  psgneldm  27437  sdrgacs  27520  compne  27653  iscusgra  28164  isuvtx  28171  isfrgra  28182  1vwmgra  28192  3vfriswmgra  28194
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-dif 3157
  Copyright terms: Public domain W3C validator