Theorem altopeq12

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

	Ref	Expression
Assertion	altopeq12	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ⟪ 𝐴 , 𝐶 ⟫ = ⟪ 𝐵 , 𝐷 ⟫ )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )
2		sneq	⊢ ( 𝐶 = 𝐷 → { 𝐶 } = { 𝐷 } )
3	1 2	anim12i	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( { 𝐴 } = { 𝐵 } ∧ { 𝐶 } = { 𝐷 } ) )
4		altopthsn	⊢ ( ⟪ 𝐴 , 𝐶 ⟫ = ⟪ 𝐵 , 𝐷 ⟫ ↔ ( { 𝐴 } = { 𝐵 } ∧ { 𝐶 } = { 𝐷 } ) )
5	3 4	sylibr	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ⟪ 𝐴 , 𝐶 ⟫ = ⟪ 𝐵 , 𝐷 ⟫ )