Theorem opeq1i

Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006)

	Ref	Expression
Hypothesis	opeq1i.1	|- A = B
Assertion	opeq1i	|- <. A , C >. = <. B , C >.

Proof

Step	Hyp	Ref	Expression
1		opeq1i.1	|- A = B
2		opeq1	|- ( A = B -> <. A , C >. = <. B , C >. )
3	1 2	ax-mp	|- <. A , C >. = <. B , C >.