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

Theorem difeq1 3287
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 2782 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3161 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3161 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2340 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684   {crab 2547    \ cdif 3149
This theorem is referenced by:  difeq12  3289  difeq1i  3290  difeq1d  3293  uneqdifeq  3542  hartogslem1  7257  kmlem9  7784  kmlem11  7786  kmlem12  7787  isfin1a  7918  fin1a2lem13  8038  incexclem  12295  ismri  13533  ablfac1eulem  15307  islbs  15829  lbsextlem1  15911  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  lpval  16871  2ndcdisj  17182  isufil  17598  ptcmplem2  17747  mblsplit  18891  voliunlem3  18909  ig1pval  19558  ballotlemgval  23082  difeq  23128  sigaval  23471  issiga  23472  issgon  23484  probun  23622  cvmscbv  23789  cvmsi  23796  cvmsval  23797  symdifeq1  24364  sssu  25141  bwt2  25592  f1otrspeq  27390  pmtrval  27394  pmtrfrn  27400  symgsssg  27408  symgfisg  27409  symggen  27411  psgnunilem1  27416  psgnunilem5  27417  psgneldm  27426  sdrgacs  27509  compne  27642  iscusgra  28153  isuvtx  28160  isfrgra  28171  1vwmgra  28181  3vfriswmgra  28183
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator