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

Theorem difeq1 3444
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 2956 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3315 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3315 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2499 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    e. wcel 1727   {crab 2715    \ cdif 3303
This theorem is referenced by:  difeq12  3446  difeq1i  3447  difeq1d  3450  uneqdifeq  3740  hartogslem1  7540  kmlem9  8069  kmlem11  8071  kmlem12  8072  isfin1a  8203  fin1a2lem13  8323  incexclem  12647  ismri  13887  ablfac1eulem  15661  islbs  16179  lbsextlem1  16261  lbsextlem2  16262  lbsextlem3  16263  lbsextlem4  16264  lpval  17234  bwth  17504  2ndcdisj  17550  isufil  17966  ptcmplem2  18115  mblsplit  19459  voliunlem3  19477  ig1pval  20126  nb3graprlem2  21492  iscusgra  21496  isuvtx  21528  difeq  24029  sigaval  24524  issiga  24525  issgon  24537  probun  24708  ballotlemgval  24812  cvmscbv  24976  cvmsi  24983  cvmsval  24984  symdifeq1  25696  f1otrspeq  27405  pmtrval  27409  pmtrfrn  27415  symgsssg  27423  symgfisg  27424  symggen  27426  psgnunilem1  27431  psgnunilem5  27432  psgneldm  27441  sdrgacs  27524  compne  27657  isfrgra  28478  1vwmgra  28491  3vfriswmgra  28493
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 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
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 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rab 2720  df-dif 3309
  Copyright terms: Public domain W3C validator