Theorem infeq2

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

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

Proof

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