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

Theorem infeq1 9516
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 9485 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
2 df-inf 9483 . 2 inf(𝐵, 𝐴, 𝑅) = sup(𝐵, 𝐴, 𝑅)
3 df-inf 9483 . 2 inf(𝐶, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
41, 2, 33eqtr4g 2802 1 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  ccnv 5684  supcsup 9480  infcinf 9481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-uni 4908  df-sup 9482  df-inf 9483
This theorem is referenced by:  infeq1d  9517  infeq1i  9518  ramcl2lem  17047  odfval  19550  odval  19552  submod  19587  ioorval  25609  uniioombllem6  25623  infleinf  45383  infxrpnf  45457  prproropf1olem2  47491  prproropf1olem3  47492  prproropf1olem4  47493  prproropf1o  47494  prproropreud  47496
  Copyright terms: Public domain W3C validator