Metamath Proof Explorer

Theorem altopeq12

Description: Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012)

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

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( A = B -> { A } = { B } )
2 sneq 
 |-  ( C = D -> { C } = { D } )
3 1 2 anim12i 
 |-  ( ( A = B /\ C = D ) -> ( { A } = { B } /\ { C } = { D } ) )
4 altopthsn 
 |-  ( << A , C >> = << B , D >> <-> ( { A } = { B } /\ { C } = { D } ) )
5 3 4 sylibr 
 |-  ( ( A = B /\ C = D ) -> << A , C >> = << B , D >> )