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

Theorem difeq1 3611
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 3103 . 2  |-  ( A  =  B  ->  { x  e.  A  |  -.  x  e.  C }  =  { x  e.  B  |  -.  x  e.  C } )
2 dfdif2 3480 . 2  |-  ( A 
\  C )  =  { x  e.  A  |  -.  x  e.  C }
3 dfdif2 3480 . 2  |-  ( B 
\  C )  =  { x  e.  B  |  -.  x  e.  C }
41, 2, 33eqtr4g 2523 1  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1395    e. wcel 1819   {crab 2811    \ cdif 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-dif 3474
This theorem is referenced by:  difeq12  3613  difeq1i  3614  difeq1d  3617  symdifeq1  3727  uneqdifeq  3919  hartogslem1  7985  kmlem9  8555  kmlem11  8557  kmlem12  8558  isfin1a  8689  fin1a2lem13  8809  incexclem  13660  ismri  15048  f1otrspeq  16599  pmtrval  16603  pmtrfrn  16610  symgsssg  16619  symgfisg  16620  symggen  16622  psgnunilem1  16645  psgnunilem5  16646  psgneldm  16655  ablfac1eulem  17250  islbs  17849  lbsextlem1  17931  lbsextlem2  17932  lbsextlem3  17933  lbsextlem4  17934  zrhcofipsgn  18756  submafval  19208  m1detdiag  19226  lpval  19767  2ndcdisj  20083  isufil  20530  ptcmplem2  20679  mblsplit  22069  voliunlem3  22088  ig1pval  22699  nb3graprlem2  24579  iscusgra  24583  isuvtx  24615  isfrgra  25117  1vwmgra  25130  3vfriswmgra  25132  difeq  27544  sigaval  28283  issiga  28284  issgon  28296  inelcarsg  28454  carsgclctunlem2  28461  probun  28555  ballotlemgval  28659  cvmscbv  28900  cvmsi  28907  cvmsval  28908  sdrgacs  31354  compne  31553  dvmptfprod  31945  ldepsnlinc  33253
  Copyright terms: Public domain W3C validator