This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opeq2i

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

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

Proof

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