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

Theorem difeq1d 4084
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 4078 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cdif 3916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-dif 3922
This theorem is referenced by:  difeq12d  4086  dffv2  6747  phplem4  8696  unfilem3  8781  marypha1lem  8894  infdifsn  9117  cantnfp1lem3  9140  en2other2  9433  isacn  9468  fin23lem28  9760  enfin1ai  9804  fin1a2lem7  9826  fzdifsuc  12971  axdc4uz  13356  leiso  13822  cshimadifsn  14191  isstruct2  16493  setsfun0  16519  strle1  16592  pltfval  17569  f1omvdco2  18576  symgsssg  18595  symgfisg  18596  symggen  18598  pmtrdifellem3  18606  pmtrdifwrdellem3  18611  pmtrdifwrdel2lem1  18612  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem1  18621  psgnunilem5  18622  psgnunilem2  18623  psgnunilem3  18624  gsumval3  19027  dmdprd  19120  dprd2da  19164  dmdprdsplit2lem  19167  dpjfval  19177  ablfac1eulem  19194  subdrgint  19582  lssset  19705  lbspropd  19871  opsrtoslem2  20265  islindf  20956  islindf2  20958  f1lindf  20966  cldval  21631  difopn  21642  mretopd  21700  restcld  21780  ordtcld1  21805  ordtcld2  21806  cnclima  21876  iscncl  21877  isreg2  21985  llycmpkgen2  22158  1stckgen  22162  ptval  22178  txcld  22211  ptcld  22221  txkgen  22260  qtopcld  22321  qtoprest  22325  qtopcmap  22327  kqcldsat  22341  regr1lem  22347  trufil  22518  ufildr  22539  opnsubg  22716  cldsubg  22719  blcld  23115  lebnumlem1  23569  bcthlem1  23931  bcth  23936  bcth3  23938  difmbl  24150  itg1val  24290  itgioo  24422  limciun  24500  dvfval  24503  istrkgl  26255  ishpg  26556  eengv  26776  elntg  26781  isuhgr  26856  isushgr  26857  uhgreq12g  26861  isuhgrop  26866  uhgr0vb  26868  uhgrun  26870  uhgrstrrepe  26874  isupgr  26880  upgrop  26890  isumgr  26891  upgrun  26914  isuspgr  26948  isusgr  26949  isuspgrop  26957  nb3grprlem2  27174  uvtxval  27180  nbupgruvtxres  27200  cplgrop  27230  cusgrexi  27236  structtocusgr  27239  1loopgrnb0  27295  isconngr1  27978  frgr3v  28063  difuncomp  30316  imadifxp  30362  gtiso  30447  difico  30517  fzdif2  30525  fzodif2  30526  fzodif1  30527  pmtrcnel2  30766  cycpmconjvlem  30815  cycpmrn  30817  tocyccntz  30818  submarchi  30847  qtophaus  31160  imambfm  31577  difelcarsg  31625  carsgclctunlem1  31632  carsggect  31633  issibf  31648  sibf0  31649  sitgfval  31656  ballotlemfval  31804  ballotlemfp1  31806  ballotlemgun  31839  hgt750lemb  31984  kur14  32520  iscvm  32563  cvmscld  32577  satf  32657  mdvval  32808  topbnd  33729  pibp21  34777  poimirlem2  35004  poimirlem4  35006  poimirlem6  35008  poimirlem7  35009  poimirlem8  35010  poimirlem11  35013  poimirlem12  35014  poimirlem13  35015  poimirlem14  35016  poimirlem16  35018  poimirlem18  35020  poimirlem19  35021  poimirlem21  35023  poimirlem22  35024  poimirlem23  35025  poimirlem27  35029  poimirlem30  35032  mblfinlem3  35041  mblfinlem4  35042  itg2addnclem  35053  itg2addnclem2  35054  prjspeclsp  39522  aomclem8  39921  kelac2  39925  gneispace2  40754  fzdifsuc2  41868  iccdifioo  42078  iccdifprioo  42079  ibliooicc  42539  dirkercncflem2  42672  issal  42882  prsal  42886  saldifcl2  42894  intsal  42896  sge0fodjrnlem  42981  caratheodorylem1  43091  vonvolmbllem  43225  salpreimagelt  43269  salpreimalegt  43271  smfresal  43346  lines  45071  rrxlines  45073  eenglngeehlnm  45079
  Copyright terms: Public domain W3C validator