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

Theorem difeq2 3288
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 2344 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21notbid 285 . . 3  |-  ( A  =  B  ->  ( -.  x  e.  A  <->  -.  x  e.  B ) )
32rabbidv 2780 . 2  |-  ( A  =  B  ->  { x  e.  C  |  -.  x  e.  A }  =  { x  e.  C  |  -.  x  e.  B } )
4 dfdif2 3161 . 2  |-  ( C 
\  A )  =  { x  e.  C  |  -.  x  e.  A }
5 dfdif2 3161 . 2  |-  ( C 
\  B )  =  { x  e.  C  |  -.  x  e.  B }
63, 4, 53eqtr4g 2340 1  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684   {crab 2547    \ cdif 3149
This theorem is referenced by:  difeq12  3289  difeq2i  3291  difeq2d  3294  ssdifeq0  3536  sorpsscmpl  6288  2oconcl  6502  oev  6513  sbthlem2  6972  sbth  6981  infdiffi  7358  fin1ai  7919  fin23lem7  7942  fin23lem11  7943  compsscnv  7997  isf34lem1  7998  compss  8002  isf34lem4  8003  fin1a2lem7  8032  pwfseqlem4a  8283  pwfseqlem4  8284  efgmval  15021  efgi  15028  frgpuptinv  15080  gsumcllem  15193  gsumzaddlem  15203  fctop  16741  cctop  16743  iscld  16764  clsval2  16787  opncldf1  16821  opncldf2  16822  opncldf3  16823  indiscld  16828  mretopd  16829  restcld  16903  lecldbas  16949  pnrmopn  17071  hauscmplem  17133  elpt  17267  elptr  17268  ptbasfi  17276  cfinfil  17588  csdfil  17589  ufilss  17600  filufint  17615  cfinufil  17623  ufinffr  17624  ufilen  17625  prdsxmslem2  18075  lebnumlem1  18459  bcth3  18753  ismbl  18885  ballotlemfval  23048  ballotlemgval  23082  iundifdifd  23159  iundifdif  23160  disjdifprg  23352  0elsiga  23475  prsiga  23492  sigaclci  23493  difelsiga  23494  kur14lem1  23737  symdifeq1  24364  isside0  26164  aishp  26172
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator