This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opthne

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
Hypotheses	opthne.1	$⊢ A \in V$
	opthne.2	$⊢ B \in V$
Assertion	opthne	$⊢ ⟨A, B⟩ \neq ⟨C, D⟩ \leftrightarrow (A \neq C \lor B \neq D)$

Proof

Step	Hyp	Ref	Expression
1		opthne.1	$⊢ A \in V$
2		opthne.2	$⊢ B \in V$
3		opthneg	$⊢ (A \in V \land B \in V) \to (⟨A, B⟩ \neq ⟨C, D⟩ \leftrightarrow (A \neq C \lor B \neq D))$
4	1 2 3	mp2an	$⊢ ⟨A, B⟩ \neq ⟨C, D⟩ \leftrightarrow (A \neq C \lor B \neq D)$