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

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 ⊢ A ∈ V ∧ B ∈ W → A B ≠ C D ↔ A ≠ C ∨ B ≠ D

Proof

Step Hyp Ref Expression
1 df-ne ⊢ A B ≠ C D ↔ ¬ A B = C D
2 opthg ⊢ A ∈ V ∧ B ∈ W → A B = C D ↔ A = C ∧ B = D
3 2 notbid ⊢ A ∈ V ∧ B ∈ W → ¬ A B = C D ↔ ¬ A = C ∧ B = D
4 ianor ⊢ ¬ A = C ∧ B = D ↔ ¬ A = C ∨ ¬ B = D
5 df-ne ⊢ A ≠ C ↔ ¬ A = C
6 df-ne ⊢ B ≠ D ↔ ¬ B = D
7 5 6 orbi12i ⊢ A ≠ C ∨ B ≠ D ↔ ¬ A = C ∨ ¬ B = D
8 4 7 bitr4i ⊢ ¬ A = C ∧ B = D ↔ A ≠ C ∨ B ≠ D
9 3 8 bitrdi ⊢ A ∈ V ∧ B ∈ W → ¬ A B = C D ↔ A ≠ C ∨ B ≠ D
10 1 9 bitrid ⊢ A ∈ V ∧ B ∈ W → A B ≠ C D ↔ A ≠ C ∨ B ≠ D