Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | opeq12 | ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 | ⊢ ( 𝐴 = 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ ) | |
2 | opeq2 | ⊢ ( 𝐵 = 𝐷 → ⟨ 𝐶 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) | |
3 | 1 2 | sylan9eq | ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) |