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

Theorem difeq2 3465
Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
difeq2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )

Proof of Theorem difeq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq2 2502 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21notbid 294 . . 3  |-  ( A  =  B  ->  ( -.  x  e.  A  <->  -.  x  e.  B ) )
32rabbidv 2962 . 2  |-  ( A  =  B  ->  { x  e.  C  |  -.  x  e.  A }  =  { x  e.  C  |  -.  x  e.  B } )
4 dfdif2 3334 . 2  |-  ( C 
\  A )  =  { x  e.  C  |  -.  x  e.  A }
5 dfdif2 3334 . 2  |-  ( C 
\  B )  =  { x  e.  C  |  -.  x  e.  B }
63, 4, 53eqtr4g 2498 1  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1364    e. wcel 1761   {crab 2717    \ cdif 3322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-ral 2718  df-rab 2722  df-dif 3328
This theorem is referenced by:  difeq12  3466  difeq2i  3468  difeq2d  3471  ssdifeq0  3758  sorpsscmpl  6370  2oconcl  6939  oev  6950  sbthlem2  7418  sbth  7427  infdiffi  7859  fin1ai  8458  fin23lem7  8481  fin23lem11  8482  compsscnv  8536  isf34lem1  8537  compss  8541  isf34lem4  8542  fin1a2lem7  8571  pwfseqlem4a  8824  pwfseqlem4  8825  efgmval  16202  efgi  16209  frgpuptinv  16261  gsumcllem  16379  gsumcllemOLD  16380  gsumzaddlem  16401  gsumzaddlemOLD  16403  fctop  18567  cctop  18569  iscld  18590  clsval2  18613  opncldf1  18647  opncldf2  18648  opncldf3  18649  indiscld  18654  mretopd  18655  restcld  18735  lecldbas  18782  pnrmopn  18906  hauscmplem  18968  elpt  19104  elptr  19105  ptbasfi  19113  cfinfil  19425  csdfil  19426  ufilss  19437  filufint  19452  cfinufil  19460  ufinffr  19461  ufilen  19462  prdsxmslem2  20063  lebnumlem1  20492  bcth3  20801  ismbl  20968  disjdifprg  25854  0elsiga  26493  prsiga  26510  sigaclci  26511  difelsiga  26512  ballotlemfval  26802  ballotlemgval  26836  kur14lem1  27024  symdifeq1  27780  frgrawopreg1  30568  frgrawopreg2  30569  bj-disjdif  32176
  Copyright terms: Public domain W3C validator