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

Theorem difeq1 3418
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 2910 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3289 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3289 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2461 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    e. wcel 1721   {crab 2670    \ cdif 3277
This theorem is referenced by:  difeq12  3420  difeq1i  3421  difeq1d  3424  uneqdifeq  3676  hartogslem1  7467  kmlem9  7994  kmlem11  7996  kmlem12  7997  isfin1a  8128  fin1a2lem13  8248  incexclem  12571  ismri  13811  ablfac1eulem  15585  islbs  16103  lbsextlem1  16185  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  lpval  17158  2ndcdisj  17472  isufil  17888  ptcmplem2  18037  mblsplit  19381  voliunlem3  19399  ig1pval  20048  nb3graprlem2  21414  iscusgra  21418  isuvtx  21450  difeq  23951  sigaval  24446  issiga  24447  issgon  24459  probun  24630  ballotlemgval  24734  cvmscbv  24898  cvmsi  24905  cvmsval  24906  symdifeq1  25578  f1otrspeq  27258  pmtrval  27262  pmtrfrn  27268  symgsssg  27276  symgfisg  27277  symggen  27279  psgnunilem1  27284  psgnunilem5  27285  psgneldm  27294  sdrgacs  27377  compne  27510  isfrgra  28094  1vwmgra  28107  3vfriswmgra  28109
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-dif 3283
  Copyright terms: Public domain W3C validator