Theorem altopeq12

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

	Ref	Expression
Assertion	altopeq12	$$⊢\left(A=B\wedge C=D\right)\to ⟪A,C⟫=⟪B,D⟫$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢A=B\to \left\{A\right\}=\left\{B\right\}$$
2		sneq	$$⊢C=D\to \left\{C\right\}=\left\{D\right\}$$
3	1 2	anim12i	$$⊢\left(A=B\wedge C=D\right)\to \left(\left\{A\right\}=\left\{B\right\}\wedge \left\{C\right\}=\left\{D\right\}\right)$$
4		altopthsn	$$⊢⟪A,C⟫=⟪B,D⟫\leftrightarrow \left(\left\{A\right\}=\left\{B\right\}\wedge \left\{C\right\}=\left\{D\right\}\right)$$
5	3 4	sylibr	$$⊢\left(A=B\wedge C=D\right)\to ⟪A,C⟫=⟪B,D⟫$$