Theorem infeq2

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

	Ref	Expression
Assertion	infeq2	⊢ ( 𝐵 = 𝐶 → inf ( 𝐴 , 𝐵 , 𝑅 ) = inf ( 𝐴 , 𝐶 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		supeq2	⊢ ( 𝐵 = 𝐶 → sup ( 𝐴 , 𝐵 , ◡ 𝑅 ) = sup ( 𝐴 , 𝐶 , ◡ 𝑅 ) )
2		df-inf	⊢ inf ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , ◡ 𝑅 )
3		df-inf	⊢ inf ( 𝐴 , 𝐶 , 𝑅 ) = sup ( 𝐴 , 𝐶 , ◡ 𝑅 )
4	1 2 3	3eqtr4g	⊢ ( 𝐵 = 𝐶 → inf ( 𝐴 , 𝐵 , 𝑅 ) = inf ( 𝐴 , 𝐶 , 𝑅 ) )