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

Theorem infeq1i 9518
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 9516 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  infcinf 9481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-uni 4908  df-sup 9482  df-inf 9483
This theorem is referenced by:  infsn  9545  nninf  12971  nn0inf  12972  lcmcom  16630  lcmass  16651  lcmf0  16671  imasdsval2  17561  imasdsf1olem  24383  ftalem6  27121  aks4d1  42090  sticksstones2  42148  supminfxr2  45480  limsup0  45709  limsupvaluz  45723  limsupmnflem  45735  limsupvaluz2  45753  limsup10ex  45788  cnrefiisp  45845  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  elaa2  46249  etransc  46298  ioorrnopn  46320  ovnval2  46560  ovolval3  46662  vonioolem2  46696
  Copyright terms: Public domain W3C validator