This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infeq1

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

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

Step	Hyp	Ref	Expression
1		supeq1	$⊢ B = C \to 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 \to inf (B, A, R) = inf (C, A, R)$