Metamath Proof Explorer

Theorem opeq12

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995)

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

Proof

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