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

Theorem infeq1i 8944
 Description: Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
Hypothesis
Ref Expression
infeq1i.1 𝐵 = 𝐶
Assertion
Ref Expression
infeq1i inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Proof of Theorem infeq1i
StepHypRef Expression
1 infeq1i.1 . 2 𝐵 = 𝐶
2 infeq1 8942 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  infcinf 8907 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-in 3890  df-ss 3900  df-uni 4805  df-sup 8908  df-inf 8909 This theorem is referenced by:  infsn  8971  nninf  12337  nn0inf  12338  lcmcom  15947  lcmass  15968  lcmf0  15988  imasdsval2  16801  imasdsf1olem  23021  ftalem6  25707  supminfxr2  42276  limsup0  42504  limsupvaluz  42518  limsupmnflem  42530  limsupvaluz2  42548  limsup10ex  42583  cnrefiisp  42640  ioodvbdlimc1lem2  42742  ioodvbdlimc2lem  42744  elaa2  43044  etransc  43093  ioorrnopn  43115  ovnval2  43352  ovolval3  43454  vonioolem2  43488
 Copyright terms: Public domain W3C validator