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

Theorem difeq1 3426
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 2918 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3297 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3297 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2469 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 2678    \ cdif 3285
This theorem is referenced by:  difeq12  3428  difeq1i  3429  difeq1d  3432  uneqdifeq  3684  hartogslem1  7475  kmlem9  8002  kmlem11  8004  kmlem12  8005  isfin1a  8136  fin1a2lem13  8256  incexclem  12579  ismri  13819  ablfac1eulem  15593  islbs  16111  lbsextlem1  16193  lbsextlem2  16194  lbsextlem3  16195  lbsextlem4  16196  lpval  17166  2ndcdisj  17480  isufil  17896  ptcmplem2  18045  mblsplit  19389  voliunlem3  19407  ig1pval  20056  nb3graprlem2  21422  iscusgra  21426  isuvtx  21458  difeq  23959  sigaval  24454  issiga  24455  issgon  24467  probun  24638  ballotlemgval  24742  cvmscbv  24906  cvmsi  24913  cvmsval  24914  symdifeq1  25586  f1otrspeq  27266  pmtrval  27270  pmtrfrn  27276  symgsssg  27284  symgfisg  27285  symggen  27287  psgnunilem1  27292  psgnunilem5  27293  psgneldm  27302  sdrgacs  27385  compne  27518  isfrgra  28102  1vwmgra  28115  3vfriswmgra  28117
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 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-dif 3291
  Copyright terms: Public domain W3C validator