Theorem supeq1i

Description: Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypothesis	supeq1i.1	|- B = C
Assertion	supeq1i	|- sup ( B , A , R ) = sup ( C , A , R )

Proof

Step	Hyp	Ref	Expression
1		supeq1i.1	|- B = C
2		supeq1	|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
3	1 2	ax-mp	|- sup ( B , A , R ) = sup ( C , A , R )