Theorem supeq1d

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

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

Proof

Step	Hyp	Ref	Expression
1		supeq1d.1	|- ( ph -> B = C )
2		supeq1	|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
3	1 2	syl	|- ( ph -> sup ( B , A , R ) = sup ( C , A , R ) )