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

Theorem difeq1 3460
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 2952 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3331 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3331 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2495 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    e. wcel 1726   {crab 2711    \ cdif 3319
This theorem is referenced by:  difeq12  3462  difeq1i  3463  difeq1d  3466  uneqdifeq  3718  hartogslem1  7514  kmlem9  8043  kmlem11  8045  kmlem12  8046  isfin1a  8177  fin1a2lem13  8297  incexclem  12621  ismri  13861  ablfac1eulem  15635  islbs  16153  lbsextlem1  16235  lbsextlem2  16236  lbsextlem3  16237  lbsextlem4  16238  lpval  17208  bwth  17478  2ndcdisj  17524  isufil  17940  ptcmplem2  18089  mblsplit  19433  voliunlem3  19451  ig1pval  20100  nb3graprlem2  21466  iscusgra  21470  isuvtx  21502  difeq  24003  sigaval  24498  issiga  24499  issgon  24511  probun  24682  ballotlemgval  24786  cvmscbv  24950  cvmsi  24957  cvmsval  24958  symdifeq1  25670  f1otrspeq  27381  pmtrval  27385  pmtrfrn  27391  symgsssg  27399  symgfisg  27400  symggen  27402  psgnunilem1  27407  psgnunilem5  27408  psgneldm  27417  sdrgacs  27500  compne  27633  isfrgra  28454  1vwmgra  28467  3vfriswmgra  28469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-dif 3325
  Copyright terms: Public domain W3C validator