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

Theorem infeq1i 8552
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 8550 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  infcinf 8515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-uni 4590  df-sup 8516  df-inf 8517
This theorem is referenced by:  infsn  8578  nninf  11983  nn0inf  11984  lcmcom  15529  lcmass  15550  lcmf0  15570  imasdsval2  16399  imasdsf1olem  22400  ftalem6  25025  supminfxr2  40216  limsup0  40448  limsupvaluz  40462  limsupmnflem  40474  limsupvaluz2  40492  limsup10ex  40527  cnrefiisp  40578  ioodvbdlimc1lem2  40669  ioodvbdlimc2lem  40671  elaa2  40973  etransc  41022  ioorrnopn  41047  ovnval2  41284  ovolval3  41386  vonioolem2  41420
  Copyright terms: Public domain W3C validator