Theorem opth1neg

Description: Two ordered pairs are not equal if their first components are not equal. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Assertion	opth1neg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≠ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		orc	⊢ ( 𝐴 ≠ 𝐶 → ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) )
2		opthneg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) ) )
3	1 2	imbitrrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≠ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ) )