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

Theorem difeq2d 3712
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 3706 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cdif 3557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2913  df-rab 2917  df-dif 3563
This theorem is referenced by:  difeq12d  3713  iinvdif  4565  otiunsndisj  4950  xpdifid  5531  imain  5942  dffv2  6238  f12dfv  6494  f13dfv  6495  tz7.49  7500  oev2  7563  difsnen  8002  domunsncan  8020  sbthlem2  8031  sbthlem3  8032  sbth  8040  phplem3  8101  phplem4  8102  unblem2  8173  unblem3  8174  xpfi  8191  dfac8alem  8812  dfac8a  8813  kmlem9  8940  kmlem11  8942  kmlem12  8943  compsscnvlem  9152  s3iunsndisj  13657  isercolllem3  14347  ruclem13  14915  bitsf1  15111  setsvalg  15827  setsval  15828  setsdm  15832  ismri2dad  16237  mreexmrid  16243  mreexexlemd  16244  gsumvalx  17210  gsumpropd  17212  gsumpropd2lem  17213  gsumress  17216  pmtrfv  17812  gsumval3a  18244  gsumval3  18248  dprdcntz  18347  dprddisj  18348  dprdsn  18375  dprddisj2  18378  dpjval  18395  ablfac1eu  18412  drngprop  18698  lbsind  19020  islbs2  19094  lbsextlem4  19101  lbsextg  19102  frlmlbs  20076  lindfind  20095  lindsind  20096  lindfrn  20100  f1lindf  20101  submaval  20327  mdetunilem3  20360  mdetunilem4  20361  mdetunilem9  20366  clsval2  20794  ntrval2  20795  ntrdif  20796  clsdif  20797  cmclsopn  20806  islp  20884  pnrmopn  21087  hauscmplem  21149  bwth  21153  conndisj  21159  cvsunit  22871  bcthlem1  23061  bcth  23066  bcth3  23068  cmmbl  23242  nulmbl2  23244  shftmbl  23246  volsup  23264  mbfimaicc  23340  eldv  23602  ig1pval  23870  tglngval  25380  axlowdimlem15  25770  axlowdim  25775  nbgr2vtx1edg  26167  nbuhgr2vtx1edgb  26169  nb3grprlem2  26204  uvtxael  26209  uvtxael1  26217  uvtxusgrel  26225  cusgredg  26241  cplgr1v  26247  cplgr3v  26252  usgredgsscusgredg  26276  usgr2pthlem  26562  2wspiundisj  26758  frcond1  27030  frgr1v  27033  nfrgr2v  27034  frgr3v  27037  1vwmgr  27038  3vfriswmgr  27040  3cyclfrgrrn1  27047  n4cyclfrgr  27053  frgrncvvdeqlem4  27064  frgrwopreglem4  27076  frgrregorufr0  27081  sigapildsyslem  30047  carsgclctunlem3  30205  sitgval  30217  ballotlemfval  30374  cvmscbv  31001  cvmsdisj  31013  cvmsss2  31017  clsun  32018  lindsenlbs  33075  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  cnambfre  33129  watvalN  34798  dnnumch1  37133  aomclem3  37145  aomclem8  37150  dssmapfv2d  37833  dssmapfv3d  37834  dssmapnvod  37835  clsk3nimkb  37859  ntrclscls00  37885  ntrclsiso  37886  ntrclsk3  37889  ntrclsk4  37891  nzprmdif  38039  compne  38164  dvmptfprodlem  39496  fouriercn  39786  meaiininclem  40037  meaiininc  40038  carageniuncllem1  40072  lindslinindsimp2  41570  ldepsnlinc  41615
  Copyright terms: Public domain W3C validator