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

Theorem infeq1i 9094
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 9092 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  infcinf 9057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-sup 9058  df-inf 9059
This theorem is referenced by:  infsn  9121  nninf  12525  nn0inf  12526  lcmcom  16150  lcmass  16171  lcmf0  16191  imasdsval2  17021  imasdsf1olem  23271  ftalem6  25960  sticksstones2  39825  supminfxr2  42684  limsup0  42910  limsupvaluz  42924  limsupmnflem  42936  limsupvaluz2  42954  limsup10ex  42989  cnrefiisp  43046  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  elaa2  43450  etransc  43499  ioorrnopn  43521  ovnval2  43758  ovolval3  43860  vonioolem2  43894
  Copyright terms: Public domain W3C validator