Theorem 3elpr2eq 4839

Description: If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.)

Assertion

Ref	Expression
3elpr2eq	⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)

Proof of Theorem 3elpr2eq

Step	Hyp	Ref	Expression
1		elpri 4591	. . 3 ⊢ (𝑋 ∈ {𝐴, 𝐵} → (𝑋 = 𝐴 ∨ 𝑋 = 𝐵))
2		elpri 4591	. . 3 ⊢ (𝑌 ∈ {𝐴, 𝐵} → (𝑌 = 𝐴 ∨ 𝑌 = 𝐵))
3		elpri 4591	. . 3 ⊢ (𝑍 ∈ {𝐴, 𝐵} → (𝑍 = 𝐴 ∨ 𝑍 = 𝐵))
4		eqtr3 2845	. . . . . . . . . . 11 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑍 = 𝑋)
5		eqneqall 3029	. . . . . . . . . . 11 ⊢ (𝑍 = 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
7	6	adantld 493	. . . . . . . . 9 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
8	7	ex 415	. . . . . . . 8 ⊢ (𝑍 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
9	8	a1d 25	. . . . . . 7 ⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
10		eqtr3 2845	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑌 = 𝑋)
11		eqneqall 3029	. . . . . . . . . . . . 13 ⊢ (𝑌 = 𝑋 → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
12	10, 11	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
13	12	impd 413	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
14	13	ex 415	. . . . . . . . . 10 ⊢ (𝑌 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
15	14	a1d 25	. . . . . . . . 9 ⊢ (𝑌 = 𝐴 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
16		eqtr3 2845	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → 𝑌 = 𝑍)
17	16	2a1d 26	. . . . . . . . . 10 ⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
18	17	ex 415	. . . . . . . . 9 ⊢ (𝑌 = 𝐵 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
19	15, 18	jaoi 853	. . . . . . . 8 ⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
20	19	com12 32	. . . . . . 7 ⊢ (𝑍 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
21	9, 20	jaoi 853	. . . . . 6 ⊢ ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
22	21	com13 88	. . . . 5 ⊢ (𝑋 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
23		eqtr3 2845	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → 𝑌 = 𝑍)
24	23	2a1d 26	. . . . . . . . . 10 ⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
25	24	ex 415	. . . . . . . . 9 ⊢ (𝑌 = 𝐴 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
26		eqtr3 2845	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑌 = 𝑋)
27	26, 11	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
28	27	impd 413	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
29	28	ex 415	. . . . . . . . . 10 ⊢ (𝑌 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
30	29	a1d 25	. . . . . . . . 9 ⊢ (𝑌 = 𝐵 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
31	25, 30	jaoi 853	. . . . . . . 8 ⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
32	31	com12 32	. . . . . . 7 ⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
33		eqtr3 2845	. . . . . . . . . . 11 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑍 = 𝑋)
34	33, 5	syl 17	. . . . . . . . . 10 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
35	34	adantld 493	. . . . . . . . 9 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
36	35	ex 415	. . . . . . . 8 ⊢ (𝑍 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
37	36	a1d 25	. . . . . . 7 ⊢ (𝑍 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
38	32, 37	jaoi 853	. . . . . 6 ⊢ ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
39	38	com13 88	. . . . 5 ⊢ (𝑋 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
40	22, 39	jaoi 853	. . . 4 ⊢ ((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
41	40	3imp 1107	. . 3 ⊢ (((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) ∧ (𝑌 = 𝐴 ∨ 𝑌 = 𝐵) ∧ (𝑍 = 𝐴 ∨ 𝑍 = 𝐵)) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
42	1, 2, 3, 41	syl3an 1156	. 2 ⊢ ((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
43	42	imp 409	1 ⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  {cpr 4571

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-v 3498  df-un 3943  df-sn 4570  df-pr 4572

This theorem is referenced by:  numedglnl  26931