Metamath Proof Explorer

Theorem altopeq2

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

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

Proof

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