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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
2 opthg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
3 2 notbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
4 ianor ⊢ ( ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( ¬ 𝐴 = 𝐶 ∨ ¬ 𝐵 = 𝐷 ) )
5 df-ne ⊢ ( 𝐴 ≠ 𝐶 ↔ ¬ 𝐴 = 𝐶 )
6 df-ne ⊢ ( 𝐵 ≠ 𝐷 ↔ ¬ 𝐵 = 𝐷 )
7 5 6 orbi12i ⊢ ( ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) ↔ ( ¬ 𝐴 = 𝐶 ∨ ¬ 𝐵 = 𝐷 ) )
8 4 7 bitr4i ⊢ ( ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) )
9 3 8 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) ) )
10 1 9 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷 ) ) )