Theorem infeq3

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

	Ref	Expression
Assertion	infeq3	|- ( R = S -> inf ( A , B , R ) = inf ( A , B , S ) )

Proof

Step	Hyp	Ref	Expression
1		cnveq	|- ( R = S -> `' R = `' S )
2		supeq3	|- ( `' R = `' S -> sup ( A , B , `' R ) = sup ( A , B , `' S ) )
3	1 2	syl	|- ( R = S -> sup ( A , B , `' R ) = sup ( A , B , `' S ) )
4		df-inf	|- inf ( A , B , R ) = sup ( A , B , `' R )
5		df-inf	|- inf ( A , B , S ) = sup ( A , B , `' S )
6	3 4 5	3eqtr4g	|- ( R = S -> inf ( A , B , R ) = inf ( A , B , S ) )