Theorem 3elpr2eq 4908

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 4651	. . 3 ⊢ (𝑋 ∈ {𝐴, 𝐵} → (𝑋 = 𝐴 ∨ 𝑋 = 𝐵))
2		elpri 4651	. . 3 ⊢ (𝑌 ∈ {𝐴, 𝐵} → (𝑌 = 𝐴 ∨ 𝑌 = 𝐵))
3		elpri 4651	. . 3 ⊢ (𝑍 ∈ {𝐴, 𝐵} → (𝑍 = 𝐴 ∨ 𝑍 = 𝐵))
4		eqtr3 2759	. . . . . . . . . . 11 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑍 = 𝑋)
5		eqneqall 2952	. . . . . . . . . . 11 ⊢ (𝑍 = 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
7	6	adantld 492	. . . . . . . . 9 ⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
8	7	ex 414	. . . . . . . 8 ⊢ (𝑍 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
9	8	a1d 25	. . . . . . 7 ⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
10		eqtr3 2759	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑌 = 𝑋)
11		eqneqall 2952	. . . . . . . . . . . . 13 ⊢ (𝑌 = 𝑋 → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
12	10, 11	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
13	12	impd 412	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
14	13	ex 414	. . . . . . . . . 10 ⊢ (𝑌 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
15	14	a1d 25	. . . . . . . . 9 ⊢ (𝑌 = 𝐴 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
16		eqtr3 2759	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → 𝑌 = 𝑍)
17	16	2a1d 26	. . . . . . . . . 10 ⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
18	17	ex 414	. . . . . . . . 9 ⊢ (𝑌 = 𝐵 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
19	15, 18	jaoi 856	. . . . . . . 8 ⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
20	19	com12 32	. . . . . . 7 ⊢ (𝑍 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
21	9, 20	jaoi 856	. . . . . 6 ⊢ ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
22	21	com13 88	. . . . 5 ⊢ (𝑋 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
23		eqtr3 2759	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → 𝑌 = 𝑍)
24	23	2a1d 26	. . . . . . . . . 10 ⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
25	24	ex 414	. . . . . . . . 9 ⊢ (𝑌 = 𝐴 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
26		eqtr3 2759	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑌 = 𝑋)
27	26, 11	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)))
28	27	impd 412	. . . . . . . . . . 11 ⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
29	28	ex 414	. . . . . . . . . 10 ⊢ (𝑌 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
30	29	a1d 25	. . . . . . . . 9 ⊢ (𝑌 = 𝐵 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
31	25, 30	jaoi 856	. . . . . . . 8 ⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
32	31	com12 32	. . . . . . 7 ⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
33		eqtr3 2759	. . . . . . . . . . 11 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑍 = 𝑋)
34	33, 5	syl 17	. . . . . . . . . 10 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))
35	34	adantld 492	. . . . . . . . 9 ⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
36	35	ex 414	. . . . . . . 8 ⊢ (𝑍 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))
37	36	a1d 25	. . . . . . 7 ⊢ (𝑍 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
38	32, 37	jaoi 856	. . . . . 6 ⊢ ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
39	38	com13 88	. . . . 5 ⊢ (𝑋 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
40	22, 39	jaoi 856	. . . 4 ⊢ ((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))))
41	40	3imp 1112	. . 3 ⊢ (((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) ∧ (𝑌 = 𝐴 ∨ 𝑌 = 𝐵) ∧ (𝑍 = 𝐴 ∨ 𝑍 = 𝐵)) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
42	1, 2, 3, 41	syl3an 1161	. 2 ⊢ ((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))
43	42	imp 408	1 ⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  numedglnl  28404