Theorem opthne 5417

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

Syntax hints:   ↔ wb 206   ∨ wo 847   ∈ wcel 2111   ≠ wne 2928  Vcvv 3436  ⟨cop 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578

This theorem is referenced by:  xpord2lem  8067  xpord2pred  8070  xpord2indlem  8072  m2detleib  22541  addsqnreup  27376  mulsval  28043  gpgedg2ov  48097  gpgedg2iv  48098  gpg5nbgrvtx03starlem1  48099  gpg5nbgrvtx03starlem2  48100  gpg5nbgrvtx03starlem3  48101  gpg5nbgrvtx13starlem1  48102  gpg5nbgrvtx13starlem2  48103  gpg5nbgrvtx13starlem3  48104  gpg3nbgrvtx0  48107  gpg3nbgrvtx0ALT  48108  gpg3nbgrvtx1  48109  gpg3kgrtriex  48120  gpgprismgr4cycllem2  48127  gpgprismgr4cycllem7  48132  gpg5edgnedg  48161  zlmodzxzldeplem  48530  line2x  48786  inlinecirc02plem  48818