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

Theorem difeq2d 4053
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 4047 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cdif 3881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-dif 3887
This theorem is referenced by:  difeq12d  4054  iinvdif  4968  otiunsndisj  5378  xpdifid  5996  imain  6413  dffv2  6737  f12dfv  7012  f13dfv  7013  tz7.49  8068  oev2  8135  difsnen  8586  domunsncan  8604  sbthlem2  8616  sbthlem3  8617  sbth  8625  phplem3  8686  phplem4  8687  unblem2  8759  unblem3  8760  xpfi  8777  dfac8alem  9444  dfac8a  9445  kmlem9  9573  kmlem11  9575  kmlem12  9576  compsscnvlem  9785  s3iunsndisj  14323  isercolllem3  15018  ruclem13  15590  bitsf1  15788  setsvalg  16507  setsval  16508  setsdm  16512  ismri2dad  16903  mreexmrid  16909  mreexexlemd  16910  gsumvalx  17881  gsumpropd  17883  gsumpropd2lem  17884  gsumress  17887  pmtrfv  18575  gsumval3a  19019  gsumval3  19023  dprdcntz  19126  dprddisj  19127  dprdsn  19154  dprddisj2  19157  dpjval  19174  ablfac1eu  19191  drngprop  19509  subdrgint  19578  lbsind  19848  islbs2  19922  lbsextlem4  19929  lbsextg  19930  frlmlbs  20489  lindfind  20508  lindsind  20509  lindfrn  20513  f1lindf  20514  submaval  21189  mdetunilem3  21222  mdetunilem4  21223  mdetunilem9  21228  clsval2  21658  ntrval2  21659  ntrdif  21660  clsdif  21661  cmclsopn  21670  islp  21748  pnrmopn  21951  hauscmplem  22014  bwth  22018  conndisj  22024  cvsunit  23739  bcthlem1  23931  bcth  23936  bcth3  23938  cmmbl  24141  nulmbl2  24143  shftmbl  24145  volsup  24163  mbfimaicc  24238  eldv  24504  ig1pval  24776  tglngval  26348  axlowdimlem15  26753  axlowdim  26758  nbgr2vtx1edg  27143  nbuhgr2vtx1edgb  27145  nb3grprlem2  27174  uvtxel  27181  uvtxel1  27189  uvtxusgrel  27196  cusgredg  27217  cplgr1v  27223  cplgr3v  27228  usgredgsscusgredg  27252  usgr2pthlem  27555  2wspiundisj  27752  frcond1  28054  frgr1v  28059  nfrgr2v  28060  frgr3v  28063  1vwmgr  28064  3vfriswmgr  28066  3cyclfrgrrn1  28073  n4cyclfrgr  28079  frgrwopreglem4a  28098  supppreima  30454  odpmco  30783  tocycfv  30804  tocycf  30812  tocyc01  30813  cycpm2tr  30814  cycpmconjslem2  30850  cyc3conja  30852  0nellinds  30989  lindssn  30996  lbslsat  31102  lindsunlem  31108  ist0cld  31186  sigapildsyslem  31528  carsgclctunlem3  31686  sitgval  31698  ballotlemfval  31855  cplgredgex  32475  cvmscbv  32613  cvmsdisj  32625  cvmsss2  32629  satfv1  32718  satffunlem  32756  satffunlem1lem1  32757  satffunlem2lem1  32759  clsun  33784  lindsadd  35043  lindsenlbs  35045  poimirlem25  35075  poimirlem26  35076  poimirlem27  35077  cnambfre  35098  watvalN  37282  dnnumch1  39975  aomclem3  39987  aomclem8  39992  dssmapfv2d  40706  dssmapfv3d  40707  dssmapnvod  40708  clsk3nimkb  40730  ntrclscls00  40756  ntrclsiso  40757  ntrclsk3  40760  ntrclsk4  40762  nzprmdif  41010  compne  41132  dvmptfprodlem  42573  fouriercn  42861  meaiininclem  43112  meaiininc  43113  carageniuncllem1  43147  lindslinindsimp2  44859  ldepsnlinc  44904  line  45133  rrxline  45135
  Copyright terms: Public domain W3C validator