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

Theorem difeq2 3615
Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
difeq2

Proof of Theorem difeq2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq2 2530 . . . 4
21notbid 294 . . 3
32rabbidv 3101 . 2
4 dfdif2 3484 . 2
5 dfdif2 3484 . 2
63, 4, 53eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818  {crab 2811  \cdif 3472
This theorem is referenced by:  difeq12  3616  difeq2i  3618  difeq2d  3621  ssdifeq0  3910  sorpsscmpl  6591  2oconcl  7172  oev  7183  sbthlem2  7648  sbth  7657  infdiffi  8095  fin1ai  8694  fin23lem7  8717  fin23lem11  8718  compsscnv  8772  isf34lem1  8773  compss  8777  isf34lem4  8778  fin1a2lem7  8807  pwfseqlem4a  9060  pwfseqlem4  9061  efgmval  16730  efgi  16737  frgpuptinv  16789  gsumcllem  16912  gsumcllemOLD  16913  gsumzaddlem  16934  gsumzaddlemOLD  16936  fctop  19505  cctop  19507  iscld  19528  clsval2  19551  opncldf1  19585  opncldf2  19586  opncldf3  19587  indiscld  19592  mretopd  19593  restcld  19673  lecldbas  19720  pnrmopn  19844  hauscmplem  19906  elpt  20073  elptr  20074  ptbasfi  20082  cfinfil  20394  csdfil  20395  ufilss  20406  filufint  20421  cfinufil  20429  ufinffr  20430  ufilen  20431  prdsxmslem2  21032  lebnumlem1  21461  bcth3  21770  ismbl  21937  frgrawopreg1  25050  frgrawopreg2  25051  disjdifprg  27436  0elsiga  28114  prsiga  28131  sigaclci  28132  difelsiga  28133  ballotlemfval  28428  ballotlemgval  28462  kur14lem1  28650  symdifeq1  29470  dvmptfprodlem  31741  bj-disjdif  34511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-rab 2816  df-dif 3478
  Copyright terms: Public domain W3C validator