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

Theorem infeq1i 8624
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 8622 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  infcinf 8587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-uni 4627  df-sup 8588  df-inf 8589
This theorem is referenced by:  infsn  8650  nninf  12010  nn0inf  12011  lcmcom  15637  lcmass  15658  lcmf0  15678  imasdsval2  16487  imasdsf1olem  22502  ftalem6  25152  supminfxr2  40429  limsup0  40657  limsupvaluz  40671  limsupmnflem  40683  limsupvaluz2  40701  limsup10ex  40736  cnrefiisp  40787  ioodvbdlimc1lem2  40878  ioodvbdlimc2lem  40880  elaa2  41181  etransc  41230  ioorrnopn  41255  ovnval2  41492  ovolval3  41594  vonioolem2  41628
  Copyright terms: Public domain W3C validator