# Metamath Proof Explorer

## 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}⟩↔\left({A}\ne {C}\vee {B}\ne {D}\right)\right)$

### Proof

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