Metamath Proof Explorer


Theorem infeq1

Description: Equality theorem for infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Assertion infeq1 B = C inf B A R = inf C A R

Proof

Step Hyp Ref Expression
1 supeq1 B = C sup B A R -1 = sup C A R -1
2 df-inf inf B A R = sup B A R -1
3 df-inf inf C A R = sup C A R -1
4 1 2 3 3eqtr4g B = C inf B A R = inf C A R