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

Theorem difeq2d 3871
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 3865 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cdif 3712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-rab 3059  df-dif 3718
This theorem is referenced by:  difeq12d  3872  iinvdif  4744  otiunsndisj  5130  xpdifid  5720  imain  6135  dffv2  6433  f12dfv  6692  f13dfv  6693  tz7.49  7709  oev2  7772  difsnen  8207  domunsncan  8225  sbthlem2  8236  sbthlem3  8237  sbth  8245  phplem3  8306  phplem4  8307  unblem2  8378  unblem3  8379  xpfi  8396  dfac8alem  9042  dfac8a  9043  kmlem9  9172  kmlem11  9174  kmlem12  9175  compsscnvlem  9384  s3iunsndisj  13908  isercolllem3  14596  ruclem13  15170  bitsf1  15370  setsvalg  16089  setsval  16090  setsdm  16094  ismri2dad  16499  mreexmrid  16505  mreexexlemd  16506  gsumvalx  17471  gsumpropd  17473  gsumpropd2lem  17474  gsumress  17477  pmtrfv  18072  gsumval3a  18504  gsumval3  18508  dprdcntz  18607  dprddisj  18608  dprdsn  18635  dprddisj2  18638  dpjval  18655  ablfac1eu  18672  drngprop  18960  lbsind  19282  islbs2  19356  lbsextlem4  19363  lbsextg  19364  frlmlbs  20338  lindfind  20357  lindsind  20358  lindfrn  20362  f1lindf  20363  submaval  20589  mdetunilem3  20622  mdetunilem4  20623  mdetunilem9  20628  clsval2  21056  ntrval2  21057  ntrdif  21058  clsdif  21059  cmclsopn  21068  islp  21146  pnrmopn  21349  hauscmplem  21411  bwth  21415  conndisj  21421  cvsunit  23131  bcthlem1  23321  bcth  23326  bcth3  23328  cmmbl  23502  nulmbl2  23504  shftmbl  23506  volsup  23524  mbfimaicc  23599  eldv  23861  ig1pval  24131  tglngval  25645  axlowdimlem15  26035  axlowdim  26040  nbgr2vtx1edg  26445  nbuhgr2vtx1edgb  26447  nb3grprlem2  26481  uvtxel  26489  uvtxaelOLD  26490  uvtxel1  26499  uvtxael1OLD  26501  uvtxusgrel  26508  cusgredg  26530  cplgr1v  26536  cplgr3v  26541  usgredgsscusgredg  26565  usgr2pthlem  26869  2wspiundisj  27085  frcond1  27420  frgr1v  27425  nfrgr2v  27426  frgr3v  27429  1vwmgr  27430  3vfriswmgr  27432  3cyclfrgrrn1  27439  n4cyclfrgr  27445  frgrwopreglem4a  27464  sigapildsyslem  30533  carsgclctunlem3  30691  sitgval  30703  ballotlemfval  30860  cvmscbv  31547  cvmsdisj  31559  cvmsss2  31563  clsun  32629  lindsenlbs  33717  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  cnambfre  33771  watvalN  35782  dnnumch1  38116  aomclem3  38128  aomclem8  38133  dssmapfv2d  38814  dssmapfv3d  38815  dssmapnvod  38816  clsk3nimkb  38840  ntrclscls00  38866  ntrclsiso  38867  ntrclsk3  38870  ntrclsk4  38872  nzprmdif  39020  compne  39145  dvmptfprodlem  40662  fouriercn  40952  meaiininclem  41206  meaiininc  41207  carageniuncllem1  41241  lindslinindsimp2  42762  ldepsnlinc  42807
  Copyright terms: Public domain W3C validator