Theorem opthne 5458

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 5457	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷)))
4	1, 2, 3	mp2an 705	1 ⊢ (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   ∈ wcel 2147   ≠ wne 2959  Vcvv 3454  ⟨cop 4840

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841

This theorem is used by:  xpord2lem  8196  xpord2pred  8199  xpord2indlem  8201  degenmgm  19187  degenmgm2  19190  m2detleib  23001  addsqnreup  27827  mulsval  28552  gpgedg2ov  49437  gpgedg2iv  49438  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem2  49443  gpg5nbgrvtx13starlem3  49444  gpg3nbgrvtx0  49447  gpg3nbgrvtx0ALT  49448  gpg3nbgrvtx1  49449  gpg3kgrtriex  49460  gpgprismgr4cycllem2  49467  gpgprismgr4cycllem7  49472  gpg5edgnedg  49501  zlmodzxzldeplem  49941