Description: Equality theorem for ordered pairs. (Contributed by NM, 28May1995)
Ref  Expression  

Assertion  opeq12   ( ( A = C /\ B = D ) > <. A , B >. = <. C , D >. ) 
Step  Hyp  Ref  Expression 

1  opeq1   ( A = C > <. A , B >. = <. C , B >. ) 

2  opeq2   ( B = D > <. C , B >. = <. C , D >. ) 

3  1 2  sylan9eq   ( ( A = C /\ B = D ) > <. A , B >. = <. C , D >. ) 