Theorem 3elpr2eq 4435

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

Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  numedglnl  26039