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

Theorem difeq2 3557
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 2529 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21notbid 300 . . 3  |-  ( A  =  B  ->  ( -.  x  e.  A  <->  -.  x  e.  B ) )
32rabbidv 3048 . 2  |-  ( A  =  B  ->  { x  e.  C  |  -.  x  e.  A }  =  { x  e.  C  |  -.  x  e.  B } )
4 dfdif2 3425 . 2  |-  ( C 
\  A )  =  { x  e.  C  |  -.  x  e.  A }
5 dfdif2 3425 . 2  |-  ( C 
\  B )  =  { x  e.  C  |  -.  x  e.  B }
63, 4, 53eqtr4g 2521 1  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1455    e. wcel 1898   {crab 2753    \ cdif 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-ral 2754  df-rab 2758  df-dif 3419
This theorem is referenced by:  difeq12  3558  difeq2i  3560  difeq2d  3563  symdifeq1  3677  disjdif2  3858  ssdifeq0  3862  sorpsscmpl  6609  2oconcl  7231  oev  7242  sbthlem2  7709  sbth  7718  infdiffi  8189  fin1ai  8749  fin23lem7  8772  fin23lem11  8773  compsscnv  8827  isf34lem1  8828  compss  8832  isf34lem4  8833  fin1a2lem7  8862  pwfseqlem4a  9112  pwfseqlem4  9113  efgmval  17411  efgi  17418  frgpuptinv  17470  gsumcllem  17591  gsumzaddlem  17603  fctop  20068  cctop  20070  iscld  20091  clsval2  20114  opncldf1  20149  opncldf2  20150  opncldf3  20151  indiscld  20156  mretopd  20157  restcld  20237  lecldbas  20284  pnrmopn  20408  hauscmplem  20470  elpt  20636  elptr  20637  cfinfil  20957  csdfil  20958  ufilss  20969  filufint  20984  cfinufil  20992  ufinffr  20993  ufilen  20994  prdsxmslem2  21593  lebnumlem1  22038  lebnumlem1OLD  22041  bcth3  22348  ismbl  22529  ishpg  24850  frgrawopreg1  25827  frgrawopreg2  25828  disjdifprg  28234  0elsiga  28985  prsiga  29002  sigaclci  29003  difelsiga  29004  unelldsys  29029  sigapildsyslem  29032  sigapildsys  29033  ldgenpisyslem1  29034  isros  29039  unelros  29042  difelros  29043  inelsros  29049  diffiunisros  29050  rossros  29051  elcarsg  29186  ballotlemfval  29371  ballotlemgval  29405  ballotlemgvalOLD  29443  kur14lem1  29978  topdifinffinlem  31795  topdifinffin  31796  prsal  38217  saldifcl  38218  salexct  38231  salexct2  38236  salexct3  38239  salgencntex  38240  salgensscntex  38241  caragenel  38354
  Copyright terms: Public domain W3C validator