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

Theorem infeq1d 8934
Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
Hypothesis
Ref Expression
infeq1d.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
infeq1d (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Proof of Theorem infeq1d
StepHypRef Expression
1 infeq1d.1 . 2 (𝜑𝐵 = 𝐶)
2 infeq1 8933 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  infcinf 8898
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-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-uni 4826  df-sup 8899  df-inf 8900
This theorem is referenced by:  limsupval  14829  lcmval  15932  lcmass  15954  lcmfval  15961  lcmf0val  15962  lcmfpr  15967  odzval  16124  ramval  16340  imasval  16782  imasdsval  16786  gexval  18701  nmofval  23318  nmoval  23319  metdsval  23450  lebnumlem1  23564  lebnumlem3  23566  ovolval  24075  ovolshft  24113  ioorf  24175  mbflimsup  24268  ig1pval  24771  elqaalem1  24913  elqaalem2  24914  elqaalem3  24915  elqaa  24916  omsval  31578  omsfval  31579  ballotlemi  31785  pellfundval  39677  dgraaval  39944  supminfrnmpt  41948  infxrpnf  41950  infxrpnf2  41968  supminfxr  41969  supminfxr2  41974  supminfxrrnmpt  41976  limsupval3  42200  limsupresre  42204  limsupresico  42208  limsuppnfdlem  42209  limsupvaluz  42216  limsupvaluzmpt  42225  liminfval  42267  liminfgval  42270  liminfval5  42273  limsupresxr  42274  liminfresxr  42275  liminfval2  42276  liminfresico  42279  liminf10ex  42282  liminfvalxr  42291  fourierdlem31  42646  ovnval  43046  ovnval2  43050  ovnval2b  43057  ovolval2  43149  ovnovollem3  43163  smfinf  43315  smfinfmpt  43316  prmdvdsfmtnof1  43970
  Copyright terms: Public domain W3C validator