Metamath Proof Explorer

Theorem altopeq1

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

Ref Expression
Assertion altopeq1 
|- ( A = B -> << A , C >> = << B , C >> )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  C = C
2 altopeq12 
 |-  ( ( A = B /\ C = C ) -> << A , C >> = << B , C >> )
3 1 2 mpan2 
 |-  ( A = B -> << A , C >> = << B , C >> )