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

Theorem difeq2d 3689
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 3683 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cdif 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ral 2900  df-rab 2904  df-dif 3542
This theorem is referenced by:  difeq12d  3690  iinvdif  4522  otiunsndisj  4896  xpdifid  5467  imain  5874  dffv2  6166  f12dfv  6407  f13dfv  6408  tz7.49  7404  oev2  7467  difsnen  7904  domunsncan  7922  sbthlem2  7933  sbthlem3  7934  sbth  7942  phplem3  8003  phplem4  8004  unblem2  8075  unblem3  8076  xpfi  8093  dfac8alem  8712  dfac8a  8713  kmlem9  8840  kmlem11  8842  kmlem12  8843  compsscnvlem  9052  s3iunsndisj  13501  isercolllem3  14191  ruclem13  14756  bitsf1  14952  setsvalg  15665  setsval  15666  setsdm  15670  ismri2dad  16066  mreexmrid  16072  mreexexlemd  16073  gsumvalx  17039  gsumpropd  17041  gsumpropd2lem  17042  gsumress  17045  pmtrfv  17641  gsumval3a  18073  gsumval3  18077  dprdcntz  18176  dprddisj  18177  dprdsn  18204  dprddisj2  18207  dpjval  18224  ablfac1eu  18241  drngprop  18527  lbsind  18847  islbs2  18921  lbsextlem4  18928  lbsextg  18929  frlmlbs  19897  lindfind  19916  lindsind  19917  lindfrn  19921  f1lindf  19922  submaval  20148  mdetunilem3  20181  mdetunilem4  20182  mdetunilem9  20187  clsval2  20606  ntrval2  20607  ntrdif  20608  clsdif  20609  cmclsopn  20618  islp  20696  pnrmopn  20899  hauscmplem  20961  bwth  20965  conndisj  20971  cvsunit  22668  bcthlem1  22846  bcth  22851  bcth3  22853  cmmbl  23026  nulmbl2  23028  shftmbl  23030  volsup  23048  mbfimaicc  23123  eldv  23385  ig1pval  23653  tglngval  25164  axlowdimlem15  25554  axlowdim  25559  nb3graprlem2  25747  cusgrarn  25754  cusgra1v  25756  cusgra2v  25757  cusgra3v  25759  usgrasscusgra  25777  sizeusglecusglem1  25778  uvtxel  25783  cusgrauvtxb  25790  frgraunss  26288  frgra1v  26291  frgra2v  26292  frgra3v  26295  1vwmgra  26296  3vfriswmgra  26298  3cyclfrgrarn1  26305  n4cyclfrgra  26311  frgrancvvdeqlem4  26326  frgrawopreglem4  26340  frgraregorufr0  26345  2spotiundisj  26355  sigapildsyslem  29357  carsgclctunlem3  29515  sitgval  29527  ballotlemfval  29684  cvmscbv  30300  cvmsdisj  30312  cvmsss2  30316  clsun  31299  lindsenlbs  32370  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  cnambfre  32424  watvalN  34093  dnnumch1  36428  aomclem3  36440  aomclem8  36445  dssmapfv2d  37128  dssmapfv3d  37129  dssmapnvod  37130  clsk3nimkb  37154  ntrclscls00  37180  ntrclsiso  37181  ntrclsk3  37184  ntrclsk4  37186  nzprmdif  37336  dvmptfprodlem  38631  fouriercn  38922  meaiininclem  39173  meaiininc  39174  carageniuncllem1  39208  nbgr2vtx1edg  40567  nbuhgr2vtx1edgb  40569  nb3grprlem2  40604  uvtxael  40609  uvtxael1  40617  uvtxusgrel  40625  cusgredg  40641  cplgr1v  40647  cplgr3v  40652  usgredgsscusgredg  40670  usgr2pthlem  40964  2wspiundisj  41161  frcond1  41433  frgr1v  41436  nfrgr2v  41437  frgr3v  41440  1vwmgr  41441  3vfriswmgr  41443  3cyclfrgrrn1  41450  n4cyclfrgr  41456  frgrncvvdeqlem4  41467  frgrwopreglem4  41479  frgrregorufr0  41484  lindslinindsimp2  42041  ldepsnlinc  42086
  Copyright terms: Public domain W3C validator