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

Theorem difeq2 3301
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 2357 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21notbid 285 . . 3  |-  ( A  =  B  ->  ( -.  x  e.  A  <->  -.  x  e.  B ) )
32rabbidv 2793 . 2  |-  ( A  =  B  ->  { x  e.  C  |  -.  x  e.  A }  =  { x  e.  C  |  -.  x  e.  B } )
4 dfdif2 3174 . 2  |-  ( C 
\  A )  =  { x  e.  C  |  -.  x  e.  A }
5 dfdif2 3174 . 2  |-  ( C 
\  B )  =  { x  e.  C  |  -.  x  e.  B }
63, 4, 53eqtr4g 2353 1  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    e. wcel 1696   {crab 2560    \ cdif 3162
This theorem is referenced by:  difeq12  3302  difeq2i  3304  difeq2d  3307  ssdifeq0  3549  sorpsscmpl  6304  2oconcl  6518  oev  6529  sbthlem2  6988  sbth  6997  infdiffi  7374  fin1ai  7935  fin23lem7  7958  fin23lem11  7959  compsscnv  8013  isf34lem1  8014  compss  8018  isf34lem4  8019  fin1a2lem7  8048  pwfseqlem4a  8299  pwfseqlem4  8300  efgmval  15037  efgi  15044  frgpuptinv  15096  gsumcllem  15209  gsumzaddlem  15219  fctop  16757  cctop  16759  iscld  16780  clsval2  16803  opncldf1  16837  opncldf2  16838  opncldf3  16839  indiscld  16844  mretopd  16845  restcld  16919  lecldbas  16965  pnrmopn  17087  hauscmplem  17149  elpt  17283  elptr  17284  ptbasfi  17292  cfinfil  17604  csdfil  17605  ufilss  17616  filufint  17631  cfinufil  17639  ufinffr  17640  ufilen  17641  prdsxmslem2  18091  lebnumlem1  18475  bcth3  18769  ismbl  18901  ballotlemfval  23064  ballotlemgval  23098  iundifdifd  23175  iundifdif  23176  disjdifprg  23367  0elsiga  23490  prsiga  23507  sigaclci  23508  difelsiga  23509  kur14lem1  23752  symdifeq1  24435  isside0  26267  aishp  26275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-rab 2565  df-dif 3168
  Copyright terms: Public domain W3C validator