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	⊢ 𝐴 ∈ V
	opthne.2	⊢ 𝐵 ∈ V
Assertion	opthne	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		opthne.1	⊢ 𝐴 ∈ V
2		opthne.2	⊢ 𝐵 ∈ V
3		opthneg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) ) )
4	1 2 3	mp2an	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) )