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

Theorem difeq1 3450
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 2942 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3321 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3321 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2492 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    e. wcel 1725   {crab 2701    \ cdif 3309
This theorem is referenced by:  difeq12  3452  difeq1i  3453  difeq1d  3456  uneqdifeq  3708  hartogslem1  7500  kmlem9  8027  kmlem11  8029  kmlem12  8030  isfin1a  8161  fin1a2lem13  8281  incexclem  12604  ismri  13844  ablfac1eulem  15618  islbs  16136  lbsextlem1  16218  lbsextlem2  16219  lbsextlem3  16220  lbsextlem4  16221  lpval  17191  bwth  17461  2ndcdisj  17507  isufil  17923  ptcmplem2  18072  mblsplit  19416  voliunlem3  19434  ig1pval  20083  nb3graprlem2  21449  iscusgra  21453  isuvtx  21485  difeq  23986  sigaval  24481  issiga  24482  issgon  24494  probun  24665  ballotlemgval  24769  cvmscbv  24933  cvmsi  24940  cvmsval  24941  symdifeq1  25619  f1otrspeq  27305  pmtrval  27309  pmtrfrn  27315  symgsssg  27323  symgfisg  27324  symggen  27326  psgnunilem1  27331  psgnunilem5  27332  psgneldm  27341  sdrgacs  27424  compne  27557  isfrgra  28238  1vwmgra  28251  3vfriswmgra  28253
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-dif 3315
  Copyright terms: Public domain W3C validator