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

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

Proof of Theorem difeq1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rabeq 3103 . 2
2 dfdif2 3484 . 2
3 dfdif2 3484 . 2
41, 2, 33eqtr4g 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  difeq1i  3617  difeq1d  3620  uneqdifeq  3916  hartogslem1  7988  kmlem9  8559  kmlem11  8561  kmlem12  8562  isfin1a  8693  fin1a2lem13  8813  incexclem  13648  ismri  15028  f1otrspeq  16472  pmtrval  16476  pmtrfrn  16483  symgsssg  16492  symgfisg  16493  symggen  16495  psgnunilem1  16518  psgnunilem5  16519  psgneldm  16528  ablfac1eulem  17123  islbs  17722  lbsextlem1  17804  lbsextlem2  17805  lbsextlem3  17806  lbsextlem4  17807  zrhcofipsgn  18629  submafval  19081  m1detdiag  19099  lpval  19640  bwthOLD  19911  2ndcdisj  19957  isufil  20404  ptcmplem2  20553  mblsplit  21943  voliunlem3  21962  ig1pval  22573  nb3graprlem2  24452  iscusgra  24456  isuvtx  24488  isfrgra  24990  1vwmgra  25003  3vfriswmgra  25005  difeq  27416  sigaval  28110  issiga  28111  issgon  28123  probun  28358  ballotlemgval  28462  cvmscbv  28703  cvmsi  28710  cvmsval  28711  symdifeq1  29470  sdrgacs  31150  compne  31349  dvmptfprod  31742  ldepsnlinc  33109
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-nfc 2607  df-rab 2816  df-dif 3478
  Copyright terms: Public domain W3C validator