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

Theorem difeq1d 3760
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 3754 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-dif 3610
This theorem is referenced by:  difeq12d  3762  diftpsn3OLD  4365  dffv2  6310  phplem4  8183  unfilem3  8267  marypha1lem  8380  infdifsn  8592  cantnfp1lem3  8615  en2other2  8870  isacn  8905  cda1dif  9036  fin23lem28  9200  enfin1ai  9244  fin1a2lem7  9266  fzdifsuc  12438  axdc4uz  12823  leiso  13281  cshimadifsn  13621  isstruct2  15914  setsfun0  15941  strle1  16020  pltfval  17006  f1omvdco2  17914  symgsssg  17933  symgfisg  17934  symggen  17936  pmtrdifellem3  17944  pmtrdifwrdellem3  17949  pmtrdifwrdel2lem1  17950  pmtrdifwrdel  17951  pmtrdifwrdel2  17952  psgnunilem1  17959  psgnunilem5  17960  psgnunilem2  17961  psgnunilem3  17962  gsumval3  18354  dmdprd  18443  dprd2da  18487  dmdprdsplit2lem  18490  dpjfval  18500  ablfac1eulem  18517  lssset  18982  lbspropd  19147  opsrtoslem2  19533  islindf  20199  islindf2  20201  f1lindf  20209  cldval  20875  difopn  20886  mretopd  20944  restcld  21024  ordtcld1  21049  ordtcld2  21050  cnclima  21120  iscncl  21121  isreg2  21229  llycmpkgen2  21401  1stckgen  21405  ptval  21421  txcld  21454  ptcld  21464  txkgen  21503  qtopcld  21564  qtoprest  21568  qtopcmap  21570  kqcldsat  21584  regr1lem  21590  trufil  21761  ufildr  21782  opnsubg  21958  cldsubg  21961  blcld  22357  lebnumlem1  22807  bcthlem1  23167  bcth  23172  bcth3  23174  difmbl  23357  itg1val  23495  itgioo  23627  limciun  23703  dvfval  23706  istrkgl  25402  ishpg  25696  eengv  25904  elntg  25909  isuhgr  26000  isushgr  26001  uhgreq12g  26005  isuhgrop  26010  uhgr0vb  26012  uhgrun  26014  uhgrstrrepe  26018  isupgr  26024  upgrop  26034  isumgr  26035  upgrun  26058  isuspgr  26092  isusgr  26093  isuspgrop  26101  nb3grprlem2  26327  uvtxval  26333  uvtxavalOLD  26334  nbupgruvtxres  26358  cplgrop  26389  cusgrexi  26395  structtocusgr  26398  1loopgrnb0  26454  isconngr1  27168  isfrgr  27238  frgr3v  27255  difuncomp  29495  imadifxp  29540  gtiso  29606  difico  29673  fzdif2  29679  fzodif2  29680  submarchi  29868  qtophaus  30031  imambfm  30452  difelcarsg  30500  carsgclctunlem1  30507  carsggect  30508  issibf  30523  sibf0  30524  sitgfval  30531  ballotlemfval  30679  ballotlemfp1  30681  ballotlemgun  30714  hgt750lemb  30862  kur14  31324  iscvm  31367  cvmscld  31381  mdvval  31527  topbnd  32444  poimirlem2  33541  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem16  33555  poimirlem18  33557  poimirlem19  33558  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem27  33566  poimirlem30  33569  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  itg2addnclem2  33592  aomclem8  37948  kelac2  37952  gneispace2  38747  fzdifsuc2  39838  iccdifioo  40059  iccdifprioo  40060  ibliooicc  40505  dirkercncflem2  40639  issal  40852  prsal  40856  saldifcl2  40864  intsal  40866  sge0fodjrnlem  40951  caratheodorylem1  41061  vonvolmbllem  41195  salpreimagelt  41239  salpreimalegt  41241  smfresal  41316
  Copyright terms: Public domain W3C validator