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

Theorem difeq2d 3621
Description: Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1d.1
Assertion
Ref Expression
difeq2d

Proof of Theorem difeq2d
StepHypRef Expression
1 difeq1d.1 . 2
2 difeq2 3615 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  \cdif 3472
This theorem is referenced by:  difeq12d  3622  iinvdif  4402  otiunsndisj  4758  xpdifid  5440  imain  5669  dffv2  5946  f12dfv  6179  f13dfv  6180  tz7.49  7129  oev2  7192  difsnen  7619  domunsncan  7637  sbthlem2  7648  sbthlem3  7649  sbth  7657  phplem3  7718  phplem4  7719  unblem2  7793  unblem3  7794  xpfi  7811  cantnffvalOLD  8103  wemapweOLD  8161  oef1oOLD  8163  dfac8alem  8431  dfac8a  8432  kmlem9  8559  kmlem11  8561  kmlem12  8562  compsscnvlem  8771  isercolllem3  13489  ruclem13  13975  bitsf1  14096  setsvalg  14655  setsval  14656  ismri2dad  15034  mreexmrid  15040  mreexexlemd  15041  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  gsumress  15903  pmtrfv  16477  gsumval3a  16905  gsumval3aOLD  16906  gsumval3OLD  16908  gsumval3  16911  gsumzsubmclOLD  16929  pwsgsumOLD  17010  dprdvalOLD  17036  dprdcntz  17041  dprddisj  17042  dprdsn  17083  dprddisj2  17087  dprddisj2OLD  17088  dpjval  17105  ablfac1eu  17124  drngprop  17407  lbsind  17726  islbs2  17800  lbsextlem4  17807  lbsextg  17808  frlmgsumOLD  18801  frlmlbs  18831  lindfind  18851  lindsind  18852  lindfrn  18856  f1lindf  18857  submaval  19083  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  clsval2  19551  ntrval2  19552  ntrdif  19553  clsdif  19554  cmclsopn  19563  cmntrcld  19564  islp  19641  pnrmopn  19844  hauscmplem  19906  bwth  19910  conndisj  19917  cvsunit  21608  bcthlem1  21763  bcth  21768  bcth3  21770  cmmbl  21945  nulmbl2  21947  shftmbl  21949  volsup  21966  mbfimaicc  22040  eldv  22302  ig1pval  22573  tglngval  23938  ishpg  24128  axlowdimlem15  24259  axlowdim  24264  nb3graprlem2  24452  cusgrarn  24459  cusgra1v  24461  cusgra2v  24462  cusgra3v  24464  usgrasscusgra  24483  sizeusglecusglem1  24484  uvtxel  24489  cusgrauvtxb  24496  frgraunss  24995  frgra1v  24998  frgra2v  24999  frgra3v  25002  1vwmgra  25003  3vfriswmgra  25005  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgrancvvdeqlem4  25033  frgrawopreglem4  25047  frgraregorufr0  25052  2spotiundisj  25062  sitgval  28274  ballotlemfval  28428  cvmscbv  28703  cvmsdisj  28715  cvmsss2  28719  cnambfre  30063  clsun  30146  dnnumch1  30990  aomclem3  31002  aomclem8  31007  mapfien2OLD  31042  nzprmdif  31224  dvmptfprodlem  31741  fouriercn  32015  usgra2pthlem1  32353  lindslinindsimp2  33064  ldepsnlinc  33109  watvalN  35717
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