Theorem opthne 5429

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

Syntax hints:   ↔ wb 206   ∨ wo 847   ∈ wcel 2109   ≠ wne 2925  Vcvv 3438  ⟨cop 4585

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  xpord2lem  8082  xpord2pred  8085  xpord2indlem  8087  m2detleib  22535  addsqnreup  27371  mulsval  28036  gpgedg2ov  48070  gpgedg2iv  48071  gpg5nbgrvtx03starlem1  48072  gpg5nbgrvtx03starlem2  48073  gpg5nbgrvtx03starlem3  48074  gpg5nbgrvtx13starlem1  48075  gpg5nbgrvtx13starlem2  48076  gpg5nbgrvtx13starlem3  48077  gpg3nbgrvtx0  48080  gpg3nbgrvtx0ALT  48081  gpg3nbgrvtx1  48082  gpg3kgrtriex  48093  gpgprismgr4cycllem2  48100  gpgprismgr4cycllem7  48105  gpg5edgnedg  48134  zlmodzxzldeplem  48503  line2x  48759  inlinecirc02plem  48791