Theorem prneimg 4859

Description: Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)

Assertion

Ref	Expression
prneimg	⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Proof of Theorem prneimg

Step	Hyp	Ref	Expression
1		preq12bg 4858	. . . . 5 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
2		orddi 1011	. . . . . 6 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) ↔ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))))
3		simpll 767	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
4		pm1.4 869	. . . . . . . 8 ⊢ ((𝐵 = 𝐷 ∨ 𝐵 = 𝐶) → (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
5	4	ad2antll 729	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
6	3, 5	jca 511	. . . . . 6 ⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
7	2, 6	sylbi 217	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
8	1, 7	biimtrdi 253	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))))
9		ianor 983	. . . . . 6 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷))
10		nne 2942	. . . . . . 7 ⊢ (¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶)
11		nne 2942	. . . . . . 7 ⊢ (¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷)
12	10, 11	orbi12i 914	. . . . . 6 ⊢ ((¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
13	9, 12	bitr2i 276	. . . . 5 ⊢ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ↔ ¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))
14		ianor 983	. . . . . 6 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷))
15		nne 2942	. . . . . . 7 ⊢ (¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶)
16		nne 2942	. . . . . . 7 ⊢ (¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷)
17	15, 16	orbi12i 914	. . . . . 6 ⊢ ((¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
18	14, 17	bitr2i 276	. . . . 5 ⊢ ((𝐵 = 𝐶 ∨ 𝐵 = 𝐷) ↔ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))
19	13, 18	anbi12i 628	. . . 4 ⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) ↔ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
20	8, 19	imbitrdi 251	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
21		pm4.56 990	. . 3 ⊢ ((¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
22	20, 21	imbitrdi 251	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → ¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
23	22	necon2ad 2953	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  prnebg  4861  opthhausdorff  5527  symg2bas  19425  m2detleib  22653  umgrvad2edg  29245  usgrexmpldifpr  29290  usgrexmpl1lem  47916  usgrexmpl2lem  47921  usgrexmpl2nb0  47926  usgrexmpl2nb1  47927  usgrexmpl2nb2  47928  usgrexmpl2nb3  47929  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  gpg5nbgrvtx03starlem1  47959  gpg5nbgrvtx03starlem2  47960  gpg5nbgrvtx03starlem3  47961  gpg5nbgrvtx13starlem1  47962  gpg5nbgrvtx13starlem2  47963  gpg5nbgrvtx13starlem3  47964  zlmodzxzldeplem  48344  line2x  48604  inlinecirc02plem  48636