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

Theorem difeq2d 4080
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 4074 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cdif 3905
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-dif 3911
This theorem is referenced by:  difeq12d  4081  iinvdif  5038  otiunsndisj  5475  xpdifid  6118  imain  6583  dffv2  6933  f12dfv  7215  f13dfv  7216  tz7.49  8387  oev2  8465  difsnen  8993  domunsncan  9012  sbthlem2  9024  sbthlem3  9025  sbth  9033  rexdif1en  9098  rexdif1enOLD  9099  dif1en  9100  dif1enOLD  9102  sbthfi  9142  phplem2  9148  phplem3OLD  9159  phplem4OLD  9160  unblem2  9236  unblem3  9237  xpfiOLD  9258  dfac8alem  9961  dfac8a  9962  kmlem9  10090  kmlem11  10092  kmlem12  10093  compsscnvlem  10302  s3iunsndisj  14845  isercolllem3  15543  ruclem13  16116  bitsf1  16318  setsvalg  17030  setsval  17031  setsdm  17034  ismri2dad  17509  mreexmrid  17515  mreexexlemd  17516  gsumvalx  18523  gsumpropd  18525  gsumpropd2lem  18526  gsumress  18529  pmtrfv  19225  gsumval3a  19671  gsumval3  19675  dprdcntz  19778  dprddisj  19779  dprdsn  19806  dprddisj2  19809  dpjval  19826  ablfac1eu  19843  drngprop  20184  subdrgint  20255  lbsind  20526  islbs2  20600  lbsextlem4  20607  lbsextg  20608  frlmlbs  21188  lindfind  21207  lindsind  21208  lindfrn  21212  f1lindf  21213  submaval  21914  mdetunilem3  21947  mdetunilem4  21948  mdetunilem9  21953  clsval2  22385  ntrval2  22386  ntrdif  22387  clsdif  22388  cmclsopn  22397  islp  22475  pnrmopn  22678  hauscmplem  22741  bwth  22745  conndisj  22751  cvsunit  24478  bcthlem1  24672  bcth  24677  bcth3  24679  cmmbl  24882  nulmbl2  24884  shftmbl  24886  volsup  24904  mbfimaicc  24979  eldv  25246  ig1pval  25521  tglngval  27379  axlowdimlem15  27791  axlowdim  27796  nbgr2vtx1edg  28184  nbuhgr2vtx1edgb  28186  nb3grprlem2  28215  uvtxel  28222  uvtxel1  28230  uvtxusgrel  28237  cusgredg  28258  cplgr1v  28264  cplgr3v  28269  usgredgsscusgredg  28293  usgr2pthlem  28597  2wspiundisj  28794  frcond1  29096  frgr1v  29101  nfrgr2v  29102  frgr3v  29105  1vwmgr  29106  3vfriswmgr  29108  3cyclfrgrrn1  29115  n4cyclfrgr  29121  frgrwopreglem4a  29140  supppreima  31490  odpmco  31820  tocycfv  31841  tocycf  31849  tocyc01  31850  cycpm2tr  31851  cycpmconjslem2  31887  cyc3conja  31889  0nellinds  32042  lindssn  32049  lbslsat  32190  lindsunlem  32196  ist0cld  32283  sigapildsyslem  32629  carsgclctunlem3  32789  sitgval  32801  ballotlemfval  32958  cplgredgex  33583  cvmscbv  33721  cvmsdisj  33733  cvmsss2  33737  satfv1  33826  satffunlem  33864  satffunlem1lem1  33865  satffunlem2lem1  33867  clsun  34767  lindsadd  36038  lindsenlbs  36040  poimirlem25  36070  poimirlem26  36071  poimirlem27  36072  cnambfre  36093  watvalN  38423  dnnumch1  41309  aomclem3  41321  aomclem8  41326  safesnsupfilb  41632  dssmapfv2d  42232  dssmapfv3d  42233  dssmapnvod  42234  clsk3nimkb  42254  ntrclscls00  42280  ntrclsiso  42281  ntrclsk3  42284  ntrclsk4  42286  nzprmdif  42541  compne  42663  dvmptfprodlem  44117  fouriercn  44405  meaiininclem  44659  meaiininc  44660  carageniuncllem1  44694  lindslinindsimp2  46476  ldepsnlinc  46521  line  46750  rrxline  46752  iscnrm3rlem4  46908
  Copyright terms: Public domain W3C validator