Theorem 3elpr2eq 4835

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 4580	. . 3 ⊢ (𝑋 ∈ {𝐴, 𝐵} → (𝑋 = 𝐴 ∨ 𝑋 = 𝐵))
2		elpri 4580	. . 3 ⊢ (𝑌 ∈ {𝐴, 𝐵} → (𝑌 = 𝐴 ∨ 𝑌 = 𝐵))
3		elpri 4580	. . 3 ⊢ (𝑍 ∈ {𝐴, 𝐵} → (𝑍 = 𝐴 ∨ 𝑍 = 𝐵))
4		eqtr3 2764	. . . . . . . . . . 11 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑍 = 𝑋)
5		eqneqall 2953	. . . . . . . . . . 11 ⊢ (𝑍 = 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
7	6	adantld 490	. . . . . . . . 9 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
8	7	ex 412	. . . . . . . 8 ⊢ (𝑍 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
9	8	a1d 25	. . . . . . 7 ⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
10		eqtr3 2764	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑌 = 𝑋)
11		eqneqall 2953	. . . . . . . . . . . . 13 ⊢ (𝑌 = 𝑋 → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
12	10, 11	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
13	12	impd 410	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
14	13	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
15	14	a1d 25	. . . . . . . . 9 ⊢ (𝑌 = 𝐴 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
16		eqtr3 2764	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → 𝑌 = 𝑍)
17	16	2a1d 26	. . . . . . . . . 10 ⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
18	17	ex 412	. . . . . . . . 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 2764	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → 𝑌 = 𝑍)
24	23	2a1d 26	. . . . . . . . . 10 ⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
25	24	ex 412	. . . . . . . . 9 ⊢ (𝑌 = 𝐴 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
26		eqtr3 2764	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑌 = 𝑋)
27	26, 11	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
28	27	impd 410	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
29	28	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
30	29	a1d 25	. . . . . . . . 9 ⊢ (𝑌 = 𝐵 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
31	25, 30	jaoi 853	. . . . . . . 8 ⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
32	31	com12 32	. . . . . . 7 ⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
33		eqtr3 2764	. . . . . . . . . . 11 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑍 = 𝑋)
34	33, 5	syl 17	. . . . . . . . . 10 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
35	34	adantld 490	. . . . . . . . 9 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
36	35	ex 412	. . . . . . . 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 1109	. . 3 ⊢ (((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) ∧ (𝑌 = 𝐴 ∨ 𝑌 = 𝐵) ∧ (𝑍 = 𝐴 ∨ 𝑍 = 𝐵)) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
42	1, 2, 3, 41	syl3an 1158	. 2 ⊢ ((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
43	42	imp 406	1 ⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  numedglnl  27417