Theorem opth2neg

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

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

Proof

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