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

Theorem infeq1 8937
Description: Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
Assertion
Ref Expression
infeq1 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Proof of Theorem infeq1
StepHypRef Expression
1 supeq1 8906 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
2 df-inf 8904 . 2 inf(𝐵, 𝐴, 𝑅) = sup(𝐵, 𝐴, 𝑅)
3 df-inf 8904 . 2 inf(𝐶, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
41, 2, 33eqtr4g 2884 1 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  ccnv 5541  supcsup 8901  infcinf 8902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-uni 4825  df-sup 8903  df-inf 8904
This theorem is referenced by:  infeq1d  8938  infeq1i  8939  ramcl2lem  16343  odfval  18660  odval  18662  submod  18694  ioorval  24181  uniioombllem6  24195  infleinf  41930  infxrpnf  42010  prproropf1olem2  43947  prproropf1olem3  43948  prproropf1olem4  43949  prproropf1o  43950  prproropreud  43952
  Copyright terms: Public domain W3C validator