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

Theorem difeq2 3451
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 2496 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21notbid 286 . . 3  |-  ( A  =  B  ->  ( -.  x  e.  A  <->  -.  x  e.  B ) )
32rabbidv 2940 . 2  |-  ( A  =  B  ->  { x  e.  C  |  -.  x  e.  A }  =  { x  e.  C  |  -.  x  e.  B } )
4 dfdif2 3321 . 2  |-  ( C 
\  A )  =  { x  e.  C  |  -.  x  e.  A }
5 dfdif2 3321 . 2  |-  ( C 
\  B )  =  { x  e.  C  |  -.  x  e.  B }
63, 4, 53eqtr4g 2492 1  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    e. wcel 1725   {crab 2701    \ cdif 3309
This theorem is referenced by:  difeq12  3452  difeq2i  3454  difeq2d  3457  ssdifeq0  3702  sorpsscmpl  6525  2oconcl  6739  oev  6750  sbthlem2  7210  sbth  7219  infdiffi  7602  fin1ai  8163  fin23lem7  8186  fin23lem11  8187  compsscnv  8241  isf34lem1  8242  compss  8246  isf34lem4  8247  fin1a2lem7  8276  pwfseqlem4a  8526  pwfseqlem4  8527  efgmval  15334  efgi  15341  frgpuptinv  15393  gsumcllem  15506  gsumzaddlem  15516  fctop  17058  cctop  17060  iscld  17081  clsval2  17104  opncldf1  17138  opncldf2  17139  opncldf3  17140  indiscld  17145  mretopd  17146  restcld  17226  lecldbas  17273  pnrmopn  17397  hauscmplem  17459  elpt  17594  elptr  17595  ptbasfi  17603  cfinfil  17915  csdfil  17916  ufilss  17927  filufint  17942  cfinufil  17950  ufinffr  17951  ufilen  17952  prdsxmslem2  18549  lebnumlem1  18976  bcth3  19274  ismbl  19412  disjdifprg  24007  0elsiga  24487  prsiga  24504  sigaclci  24505  difelsiga  24506  ballotlemfval  24737  ballotlemgval  24771  kur14lem1  24882  symdifeq1  25630  frgrawopreg1  28340  frgrawopreg2  28341
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-rab 2706  df-dif 3315
  Copyright terms: Public domain W3C validator