Theorem opthneg

Description: Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢⟨A,B⟩\ne ⟨C,D⟩\leftrightarrow \neg ⟨A,B⟩=⟨C,D⟩$$
2		opthg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)\right)$$
3	2	notbid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg ⟨A,B⟩=⟨C,D⟩\leftrightarrow \neg \left(A=C\wedge B=D\right)\right)$$
4		ianor	$$⊢\neg \left(A=C\wedge B=D\right)\leftrightarrow \left(\neg A=C\vee \neg B=D\right)$$
5		df-ne	$$⊢A\ne C\leftrightarrow \neg A=C$$
6		df-ne	$$⊢B\ne D\leftrightarrow \neg B=D$$
7	5 6	orbi12i	$$⊢\left(A\ne C\vee B\ne D\right)\leftrightarrow \left(\neg A=C\vee \neg B=D\right)$$
8	4 7	bitr4i	$$⊢\neg \left(A=C\wedge B=D\right)\leftrightarrow \left(A\ne C\vee B\ne D\right)$$
9	3 8	bitrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg ⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A\ne C\vee B\ne D\right)\right)$$
10	1 9	syl5bb	$$⊢\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)$$