Metamath Proof Explorer


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 >.