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

Theorem difeq2d 3934
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 3928 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cdif 3773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-ral 3108  df-rab 3112  df-dif 3779
This theorem is referenced by:  difeq12d  3935  iinvdif  4791  otiunsndisj  5182  xpdifid  5780  imain  6188  dffv2  6495  f12dfv  6756  f13dfv  6757  tz7.49  7779  oev2  7843  difsnen  8284  domunsncan  8302  sbthlem2  8313  sbthlem3  8314  sbth  8322  phplem3  8383  phplem4  8384  unblem2  8455  unblem3  8456  xpfi  8473  dfac8alem  9138  dfac8a  9139  kmlem9  9268  kmlem11  9270  kmlem12  9271  compsscnvlem  9480  s3iunsndisj  13935  isercolllem3  14623  ruclem13  15194  bitsf1  15390  setsvalg  16101  setsval  16102  setsdm  16106  ismri2dad  16505  mreexmrid  16511  mreexexlemd  16512  gsumvalx  17478  gsumpropd  17480  gsumpropd2lem  17481  gsumress  17484  pmtrfv  18076  gsumval3a  18508  gsumval3  18512  dprdcntz  18612  dprddisj  18613  dprdsn  18640  dprddisj2  18643  dpjval  18660  ablfac1eu  18677  drngprop  18965  lbsind  19290  islbs2  19366  lbsextlem4  19373  lbsextg  19374  frlmlbs  20350  lindfind  20369  lindsind  20370  lindfrn  20374  f1lindf  20375  submaval  20602  mdetunilem3  20635  mdetunilem4  20636  mdetunilem9  20641  clsval2  21072  ntrval2  21073  ntrdif  21074  clsdif  21075  cmclsopn  21084  islp  21162  pnrmopn  21365  hauscmplem  21427  bwth  21431  conndisj  21437  cvsunit  23147  bcthlem1  23338  bcth  23343  bcth3  23345  cmmbl  23521  nulmbl2  23523  shftmbl  23525  volsup  23543  mbfimaicc  23618  eldv  23882  ig1pval  24152  tglngval  25666  axlowdimlem15  26056  axlowdim  26061  nbgr2vtx1edg  26468  nbuhgr2vtx1edgb  26470  nb3grprlem2  26505  uvtxel  26513  uvtxaelOLD  26514  uvtxel1  26523  uvtxael1OLD  26525  uvtxusgrel  26532  cusgredg  26554  cplgr1v  26560  cplgr3v  26565  usgredgsscusgredg  26589  usgr2pthlem  26893  2wspiundisj  27111  frcond1  27447  frgr1v  27452  nfrgr2v  27453  frgr3v  27456  1vwmgr  27457  3vfriswmgr  27459  3cyclfrgrrn1  27466  n4cyclfrgr  27472  frgrwopreglem4a  27491  sigapildsyslem  30555  carsgclctunlem3  30713  sitgval  30725  ballotlemfval  30882  cvmscbv  31568  cvmsdisj  31580  cvmsss2  31584  clsun  32649  lindsenlbs  33719  poimirlem25  33749  poimirlem26  33750  poimirlem27  33751  cnambfre  33772  watvalN  35775  dnnumch1  38116  aomclem3  38128  aomclem8  38133  dssmapfv2d  38813  dssmapfv3d  38814  dssmapnvod  38815  clsk3nimkb  38839  ntrclscls00  38865  ntrclsiso  38866  ntrclsk3  38869  ntrclsk4  38871  nzprmdif  39019  compne  39143  dvmptfprodlem  40640  fouriercn  40929  meaiininclem  41183  meaiininc  41184  carageniuncllem1  41218  lindslinindsimp2  42821  ldepsnlinc  42866
  Copyright terms: Public domain W3C validator