Theorem prneimg 4812

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 4811	. . . . 5 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
2		orddi 1012	. . . . . 6 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) ↔ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))))
3		simpll 767	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
4		pm1.4 870	. . . . . . . 8 ⊢ ((𝐵 = 𝐷 ∨ 𝐵 = 𝐶) → (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
5	4	ad2antll 730	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
6	3, 5	jca 511	. . . . . 6 ⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
7	2, 6	sylbi 217	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
8	1, 7	biimtrdi 253	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))))
9		ianor 984	. . . . . 6 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷))
10		nne 2937	. . . . . . 7 ⊢ (¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶)
11		nne 2937	. . . . . . 7 ⊢ (¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷)
12	10, 11	orbi12i 915	. . . . . 6 ⊢ ((¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
13	9, 12	bitr2i 276	. . . . 5 ⊢ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ↔ ¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))
14		ianor 984	. . . . . 6 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷))
15		nne 2937	. . . . . . 7 ⊢ (¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶)
16		nne 2937	. . . . . . 7 ⊢ (¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷)
17	15, 16	orbi12i 915	. . . . . 6 ⊢ ((¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
18	14, 17	bitr2i 276	. . . . 5 ⊢ ((𝐵 = 𝐶 ∨ 𝐵 = 𝐷) ↔ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))
19	13, 18	anbi12i 629	. . . 4 ⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) ↔ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
20	8, 19	imbitrdi 251	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
21		pm4.56 991	. . 3 ⊢ ((¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
22	20, 21	imbitrdi 251	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → ¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
23	22	necon2ad 2948	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  prnebg  4814  opthhausdorff  5475  symg2bas  19339  m2detleib  22592  umgrvad2edg  29304  usgrexmpldifpr  29349  usgrexmpl1lem  48410  usgrexmpl2lem  48415  usgrexmpl2nb0  48420  usgrexmpl2nb1  48421  usgrexmpl2nb2  48422  usgrexmpl2nb3  48423  usgrexmpl2nb4  48424  usgrexmpl2nb5  48425  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  gpgprismgr4cycllem2  48485  gpg5edgnedg  48519  zlmodzxzldeplem  48887  line2x  49143  inlinecirc02plem  49175