Theorem infeq1

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

	Ref	Expression
Assertion	infeq1	$$⊢B=C\to inf\left(B,A,R\right)=inf\left(C,A,R\right)$$

Proof

Step	Hyp	Ref	Expression
1		supeq1	$$⊢B=C\to sup\left(B,A,R^{-1}\right)=sup\left(C,A,R^{-1}\right)$$
2		df-inf	$$⊢inf\left(B,A,R\right)=sup\left(B,A,R^{-1}\right)$$
3		df-inf	$$⊢inf\left(C,A,R\right)=sup\left(C,A,R^{-1}\right)$$
4	1 2 3	3eqtr4g	$$⊢B=C\to inf\left(B,A,R\right)=inf\left(C,A,R\right)$$