Theorem opthne 5462

Description: Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.)

Hypotheses

Ref	Expression
opthne.1	⊢ 𝐴 ∈ V
opthne.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
opthne	⊢ (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷))

Proof of Theorem opthne

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

Syntax hints:   ↔ wb 206   ∨ wo 847   ∈ wcel 2109   ≠ wne 2933  Vcvv 3464  ⟨cop 4612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613

This theorem is referenced by:  xpord2lem  8146  xpord2pred  8149  xpord2indlem  8151  m2detleib  22574  addsqnreup  27411  mulsval  28069  gpg5nbgrvtx03starlem1  48037  gpg5nbgrvtx03starlem2  48038  gpg5nbgrvtx03starlem3  48039  gpg5nbgrvtx13starlem1  48040  gpg5nbgrvtx13starlem2  48041  gpg5nbgrvtx13starlem3  48042  gpg3nbgrvtx0  48045  gpg3nbgrvtx0ALT  48046  gpg3nbgrvtx1  48047  gpg3kgrtriex  48058  gpgprismgr4cycllem2  48062  gpgprismgr4cycllem7  48067  zlmodzxzldeplem  48441  line2x  48701  inlinecirc02plem  48733