Theorem infeq1

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

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

Proof

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