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

Theorem infeq1i 8930
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 8928 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  infcinf 8893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ral 3140  df-rex 3141  df-rab 3144  df-uni 4831  df-sup 8894  df-inf 8895
This theorem is referenced by:  infsn  8957  nninf  12317  nn0inf  12318  lcmcom  15925  lcmass  15946  lcmf0  15966  imasdsval2  16777  imasdsf1olem  22910  ftalem6  25582  supminfxr2  41621  limsup0  41851  limsupvaluz  41865  limsupmnflem  41877  limsupvaluz2  41895  limsup10ex  41930  cnrefiisp  41987  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  elaa2  42396  etransc  42445  ioorrnopn  42467  ovnval2  42704  ovolval3  42806  vonioolem2  42840
  Copyright terms: Public domain W3C validator