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

Theorem difeq1d 3926
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 3920 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cdif 3766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-dif 3772
This theorem is referenced by:  difeq12d  3928  dffv2  6492  phplem4  8381  unfilem3  8465  marypha1lem  8578  infdifsn  8801  cantnfp1lem3  8824  en2other2  9115  isacn  9150  cda1dif  9283  fin23lem28  9447  enfin1ai  9491  fin1a2lem7  9513  fzdifsuc  12623  axdc4uz  13007  leiso  13460  cshimadifsn  13799  isstruct2  16078  setsfun0  16105  strle1  16184  pltfval  17164  f1omvdco2  18069  symgsssg  18088  symgfisg  18089  symggen  18091  pmtrdifellem3  18099  pmtrdifwrdellem3  18104  pmtrdifwrdel2lem1  18105  pmtrdifwrdel  18106  pmtrdifwrdel2  18107  psgnunilem1  18114  psgnunilem5  18115  psgnunilem2  18116  psgnunilem3  18117  gsumval3  18509  dmdprd  18599  dprd2da  18643  dmdprdsplit2lem  18646  dpjfval  18656  ablfac1eulem  18673  lssset  19138  lbspropd  19306  opsrtoslem2  19693  islindf  20361  islindf2  20363  f1lindf  20371  cldval  21041  difopn  21052  mretopd  21110  restcld  21190  ordtcld1  21215  ordtcld2  21216  cnclima  21286  iscncl  21287  isreg2  21395  llycmpkgen2  21567  1stckgen  21571  ptval  21587  txcld  21620  ptcld  21630  txkgen  21669  qtopcld  21730  qtoprest  21734  qtopcmap  21736  kqcldsat  21750  regr1lem  21756  trufil  21927  ufildr  21948  opnsubg  22124  cldsubg  22127  blcld  22523  lebnumlem1  22973  bcthlem1  23333  bcth  23338  bcth3  23340  difmbl  23524  itg1val  23664  itgioo  23796  limciun  23872  dvfval  23875  istrkgl  25571  ishpg  25865  eengv  26073  elntg  26078  isuhgr  26169  isushgr  26170  uhgreq12g  26174  isuhgrop  26179  uhgr0vb  26181  uhgrun  26183  uhgrstrrepe  26187  isupgr  26193  upgrop  26203  isumgr  26204  upgrun  26227  isuspgr  26262  isusgr  26263  isuspgrop  26271  nb3grprlem2  26499  uvtxval  26505  uvtxavalOLD  26506  nbupgruvtxres  26530  cplgrop  26561  cusgrexi  26567  structtocusgr  26570  1loopgrnb0  26626  isconngr1  27363  isfrgr  27433  frgr3v  27450  difuncomp  29694  imadifxp  29739  gtiso  29805  difico  29872  fzdif2  29878  fzodif2  29879  submarchi  30065  qtophaus  30228  imambfm  30649  difelcarsg  30697  carsgclctunlem1  30704  carsggect  30705  issibf  30720  sibf0  30721  sitgfval  30728  ballotlemfval  30876  ballotlemfp1  30878  ballotlemgun  30911  hgt750lemb  31059  kur14  31521  iscvm  31564  cvmscld  31578  mdvval  31724  topbnd  32640  poimirlem2  33724  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem11  33733  poimirlem12  33734  poimirlem13  33735  poimirlem14  33736  poimirlem16  33738  poimirlem18  33740  poimirlem19  33741  poimirlem21  33743  poimirlem22  33744  poimirlem23  33745  poimirlem27  33749  poimirlem30  33752  mblfinlem3  33761  mblfinlem4  33762  itg2addnclem  33773  itg2addnclem2  33774  aomclem8  38132  kelac2  38136  gneispace2  38930  fzdifsuc2  40005  iccdifioo  40222  iccdifprioo  40223  ibliooicc  40666  dirkercncflem2  40800  issal  41013  prsal  41017  saldifcl2  41025  intsal  41027  sge0fodjrnlem  41112  caratheodorylem1  41222  vonvolmbllem  41356  salpreimagelt  41400  salpreimalegt  41402  smfresal  41477
  Copyright terms: Public domain W3C validator