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

Theorem difeq2d 3761
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 3755 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-rab 2950  df-dif 3610
This theorem is referenced by:  difeq12d  3762  iinvdif  4624  otiunsndisj  5009  xpdifid  5597  imain  6012  dffv2  6310  f12dfv  6569  f13dfv  6570  tz7.49  7585  oev2  7648  difsnen  8083  domunsncan  8101  sbthlem2  8112  sbthlem3  8113  sbth  8121  phplem3  8182  phplem4  8183  unblem2  8254  unblem3  8255  xpfi  8272  dfac8alem  8890  dfac8a  8891  kmlem9  9018  kmlem11  9020  kmlem12  9021  compsscnvlem  9230  s3iunsndisj  13753  isercolllem3  14441  ruclem13  15015  bitsf1  15215  setsvalg  15934  setsval  15935  setsdm  15939  ismri2dad  16344  mreexmrid  16350  mreexexlemd  16351  gsumvalx  17317  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  pmtrfv  17918  gsumval3a  18350  gsumval3  18354  dprdcntz  18453  dprddisj  18454  dprdsn  18481  dprddisj2  18484  dpjval  18501  ablfac1eu  18518  drngprop  18806  lbsind  19128  islbs2  19202  lbsextlem4  19209  lbsextg  19210  frlmlbs  20184  lindfind  20203  lindsind  20204  lindfrn  20208  f1lindf  20209  submaval  20435  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  clsval2  20902  ntrval2  20903  ntrdif  20904  clsdif  20905  cmclsopn  20914  islp  20992  pnrmopn  21195  hauscmplem  21257  bwth  21261  conndisj  21267  cvsunit  22977  bcthlem1  23167  bcth  23172  bcth3  23174  cmmbl  23348  nulmbl2  23350  shftmbl  23352  volsup  23370  mbfimaicc  23445  eldv  23707  ig1pval  23977  tglngval  25491  axlowdimlem15  25881  axlowdim  25886  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  nb3grprlem2  26327  uvtxel  26335  uvtxaelOLD  26336  uvtxel1  26345  uvtxael1OLD  26347  uvtxusgrel  26354  cusgredg  26376  cplgr1v  26382  cplgr3v  26387  usgredgsscusgredg  26411  usgr2pthlem  26715  2wspiundisj  26930  frcond1  27246  frgr1v  27251  nfrgr2v  27252  frgr3v  27255  1vwmgr  27256  3vfriswmgr  27258  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrwopreglem4a  27290  sigapildsyslem  30352  carsgclctunlem3  30510  sitgval  30522  ballotlemfval  30679  cvmscbv  31366  cvmsdisj  31378  cvmsss2  31382  clsun  32448  lindsenlbs  33534  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  cnambfre  33588  watvalN  35597  dnnumch1  37931  aomclem3  37943  aomclem8  37948  dssmapfv2d  38629  dssmapfv3d  38630  dssmapnvod  38631  clsk3nimkb  38655  ntrclscls00  38681  ntrclsiso  38682  ntrclsk3  38685  ntrclsk4  38687  nzprmdif  38835  compne  38960  dvmptfprodlem  40477  fouriercn  40767  meaiininclem  41021  meaiininc  41022  carageniuncllem1  41056  lindslinindsimp2  42577  ldepsnlinc  42622
  Copyright terms: Public domain W3C validator