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

Theorem difeq1 3401
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 2893 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3272 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3272 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2444 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    e. wcel 1717   {crab 2653    \ cdif 3260
This theorem is referenced by:  difeq12  3403  difeq1i  3404  difeq1d  3407  uneqdifeq  3659  hartogslem1  7444  kmlem9  7971  kmlem11  7973  kmlem12  7974  isfin1a  8105  fin1a2lem13  8225  incexclem  12543  ismri  13783  ablfac1eulem  15557  islbs  16075  lbsextlem1  16157  lbsextlem2  16158  lbsextlem3  16159  lbsextlem4  16160  lpval  17126  2ndcdisj  17440  isufil  17856  ptcmplem2  18005  mblsplit  19295  voliunlem3  19313  ig1pval  19962  nb3graprlem2  21327  iscusgra  21331  isuvtx  21363  difeq  23842  sigaval  24289  issiga  24290  issgon  24302  probun  24456  ballotlemgval  24560  cvmscbv  24724  cvmsi  24731  cvmsval  24732  symdifeq1  25388  f1otrspeq  27059  pmtrval  27063  pmtrfrn  27069  symgsssg  27077  symgfisg  27078  symggen  27080  psgnunilem1  27085  psgnunilem5  27086  psgneldm  27095  sdrgacs  27178  compne  27311  isfrgra  27743  1vwmgra  27756  3vfriswmgra  27758
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-dif 3266
  Copyright terms: Public domain W3C validator