Theorem prnebg 4805

Description: A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.)

Assertion

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

Proof of Theorem prnebg

Step	Hyp	Ref	Expression
1		prneimg 4803	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
2	1	3adant3 1132	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
3		ioran 985	. . . . 5 ⊢ (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
4		ianor 983	. . . . . . 7 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷))
5		nne 2932	. . . . . . . 8 ⊢ (¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶)
6		nne 2932	. . . . . . . 8 ⊢ (¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷)
7	5, 6	orbi12i 914	. . . . . . 7 ⊢ ((¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
8	4, 7	bitri 275	. . . . . 6 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
9		ianor 983	. . . . . . 7 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷))
10		nne 2932	. . . . . . . 8 ⊢ (¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶)
11		nne 2932	. . . . . . . 8 ⊢ (¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷)
12	10, 11	orbi12i 914	. . . . . . 7 ⊢ ((¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
13	9, 12	bitri 275	. . . . . 6 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
14	8, 13	anbi12i 628	. . . . 5 ⊢ ((¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
15	3, 14	bitri 275	. . . 4 ⊢ (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
16		anddi 1012	. . . . 5 ⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) ↔ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))))
17		eqtr3 2753	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
18		eqneqall 2939	. . . . . . . . . 10 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
19	17, 18	syl 17	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
20		preq12 4685	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
21	20	a1d 25	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
22	19, 21	jaoi 857	. . . . . . . 8 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
23		preq12 4685	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶})
24		prcom 4682	. . . . . . . . . . 11 ⊢ {𝐷, 𝐶} = {𝐶, 𝐷}
25	23, 24	eqtrdi 2782	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷})
26	25	a1d 25	. . . . . . . . 9 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
27		eqtr3 2753	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐵)
28	27, 18	syl 17	. . . . . . . . 9 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
29	26, 28	jaoi 857	. . . . . . . 8 ⊢ (((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
30	22, 29	jaoi 857	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
31	30	com12 32	. . . . . 6 ⊢ (𝐴 ≠ 𝐵 → ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
32	31	3ad2ant3 1135	. . . . 5 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
33	16, 32	biimtrid 242	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
34	15, 33	biimtrid 242	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
35	34	necon1ad 2945	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} → ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
36	2, 35	impbid 212	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  {cpr 4575

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  zlmodzxznm  48597