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	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\ne C\to ⟨A,B⟩\ne ⟨C,D⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		orc	$$⊢A\ne C\to \left(A\ne C\vee B\ne D\right)$$
2		opthneg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩\ne ⟨C,D⟩\leftrightarrow \left(A\ne C\vee B\ne D\right)\right)$$
3	1 2	imbitrrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\ne C\to ⟨A,B⟩\ne ⟨C,D⟩\right)$$