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