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

Theorem difeq1d 3688
Description: Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
difeq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem difeq1d
StepHypRef Expression
1 difeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 difeq1 3682 . 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-nfc 2739  df-rab 2904  df-dif 3542
This theorem is referenced by:  difeq12d  3690  diftpsn3OLD  4273  dffv2  6165  phplem4  8004  unfilem3  8088  marypha1lem  8199  infdifsn  8414  cantnfp1lem3  8437  en2other2  8692  isacn  8727  cda1dif  8858  fin23lem28  9022  enfin1ai  9066  fin1a2lem7  9088  fzdifsuc  12227  axdc4uz  12602  leiso  13054  cshimadifsn  13374  isstruct2  15652  setsfun0  15674  strle1  15748  pltfval  16730  f1omvdco2  17639  symgsssg  17658  symgfisg  17659  symggen  17661  pmtrdifellem3  17669  pmtrdifwrdellem3  17674  pmtrdifwrdel2lem1  17675  pmtrdifwrdel  17676  pmtrdifwrdel2  17677  psgnunilem1  17684  psgnunilem5  17685  psgnunilem2  17686  psgnunilem3  17687  gsumval3  18079  dmdprd  18168  dprd2da  18212  dmdprdsplit2lem  18215  dpjfval  18225  ablfac1eulem  18242  lssset  18703  lbspropd  18868  opsrtoslem2  19254  islindf  19917  islindf2  19919  f1lindf  19927  cldval  20584  difopn  20595  mretopd  20653  restcld  20733  ordtcld1  20758  ordtcld2  20759  cnclima  20829  iscncl  20830  isreg2  20938  llycmpkgen2  21110  1stckgen  21114  ptval  21130  txcld  21163  ptcld  21173  txkgen  21212  qtopcld  21273  qtoprest  21277  qtopcmap  21279  kqcldsat  21293  regr1lem  21299  trufil  21471  ufildr  21492  opnsubg  21668  cldsubg  21671  blcld  22067  lebnumlem1  22515  bcthlem1  22873  bcth  22878  bcth3  22880  difmbl  23062  itg1val  23200  itgioo  23332  limciun  23408  dvfval  23411  istrkgl  25101  ishpg  25396  eengv  25604  elntg  25609  isuhgra  25620  isushgra  25623  uhgrac  25627  uhgraeq12d  25629  isumgra  25637  isuslgra  25665  isusgra  25666  usgraeq12d  25684  nb3graprlem2  25774  cusgra3v  25786  isconngra1  25994  frgra3v  26322  difuncomp  28545  imadifxp  28589  gtiso  28654  difico  28728  fzdif2  28732  submarchi  28864  qtophaus  29024  imambfm  29444  difelcarsg  29492  carsgclctunlem1  29499  carsggect  29500  issibf  29515  sibf0  29516  sitgfval  29523  ballotlemfval  29671  ballotlemfp1  29673  ballotlemgun  29706  kur14  30245  iscvm  30288  cvmscld  30302  mdvval  30448  topbnd  31282  poimirlem2  32364  poimirlem4  32366  poimirlem6  32368  poimirlem7  32369  poimirlem8  32370  poimirlem11  32373  poimirlem12  32374  poimirlem13  32375  poimirlem14  32376  poimirlem16  32378  poimirlem18  32380  poimirlem19  32381  poimirlem21  32383  poimirlem22  32384  poimirlem23  32385  poimirlem27  32389  poimirlem30  32392  mblfinlem3  32401  mblfinlem4  32402  itg2addnclem  32414  itg2addnclem2  32415  aomclem8  36432  kelac2  36436  gneispace2  37233  fzdifsuc2  38249  iccdifioo  38371  iccdifprioo  38372  ibliooicc  38646  dirkercncflem2  38780  issal  38993  prsal  38997  saldifcl2  39005  intsal  39007  sge0fodjrnlem  39092  caratheodorylem1  39199  vonvolmbllem  39333  salpreimagelt  39378  salpreimalegt  39380  smfresal  39456  isuhgr  40263  isushgr  40264  uhgreq12g  40268  uhgruhgra  40273  uhgrauhgr  40274  isuhgrop  40276  uhgr0vb  40278  uhgrun  40280  uhgrstrrepe  40285  isupgr  40291  isumgr  40301  upgrun  40324  isuspgr  40363  isusgr  40364  nb3grprlem2  40590  uvtxaval  40594  nbupgruvtxres  40615  cplgrop  40640  cusgrexi  40643  1loopgrnb0  40698  isconngr1  41338  isfrgr  41411  frgr3v  41426
  Copyright terms: Public domain W3C validator