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

Proof

Step	Hyp	Ref	Expression
1		olc	$$⊢B\ne D\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(B\ne D\to ⟨A,B⟩\ne ⟨C,D⟩\right)$$