Metamath Proof Explorer

Theorem euoreqb

Description: There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023)

Ref Expression
Assertion euoreqb ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
2 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐵 ↔ 𝑦 = 𝐵 ) )
3 1 2 orbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) )
4 3 reu8 ⊢ ( ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑉 ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) ) )
5 simprlr ⊢ ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
6 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = 𝐴 ↔ 𝐵 = 𝐴 ) )
7 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = 𝐵 ↔ 𝐵 = 𝐵 ) )
8 6 7 orbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) )
9 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐵 ) )
10 8 9 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) → 𝑥 = 𝐵 ) ) )
11 10 rspcv ⊢ ( 𝐵 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) → 𝑥 = 𝐵 ) ) )
12 5 11 syl ⊢ ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) → 𝑥 = 𝐵 ) ) )
13 ioran ⊢ ( ¬ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ↔ ( ¬ 𝐵 = 𝐴 ∧ ¬ 𝐵 = 𝐵 ) )
14 eqid ⊢ 𝐵 = 𝐵
15 14 pm2.24i ⊢ ( ¬ 𝐵 = 𝐵 → ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
16 13 15 simplbiim ⊢ ( ¬ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) → ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
17 eqtr2 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → 𝐴 = 𝐵 )
18 17 ancoms ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 = 𝐴 ) → 𝐴 = 𝐵 )
19 18 a1d ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑥 = 𝐴 ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → 𝐴 = 𝐵 ) )
20 19 expimpd ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
21 16 20 ja ⊢ ( ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) → 𝑥 = 𝐵 ) → ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
22 21 com12 ⊢ ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) → 𝑥 = 𝐵 ) → 𝐴 = 𝐵 ) )
23 12 22 syld ⊢ ( ( 𝑥 = 𝐴 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) )
24 23 ex ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) ) )
25 simprll ⊢ ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
26 eqeq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐴 ↔ 𝐴 = 𝐴 ) )
27 eqeq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝐴 = 𝐵 ) )
28 26 27 orbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ↔ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ) )
29 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
30 28 29 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) → 𝑥 = 𝐴 ) ) )
31 30 rspcv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) → 𝑥 = 𝐴 ) ) )
32 25 31 syl ⊢ ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) → 𝑥 = 𝐴 ) ) )
33 ioran ⊢ ( ¬ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ↔ ( ¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵 ) )
34 eqid ⊢ 𝐴 = 𝐴
35 34 pm2.24i ⊢ ( ¬ 𝐴 = 𝐴 → ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
36 35 adantr ⊢ ( ( ¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵 ) → ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
37 33 36 sylbi ⊢ ( ¬ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) → ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
38 17 a1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → 𝐴 = 𝐵 ) )
39 38 expimpd ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
40 37 39 ja ⊢ ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) → 𝑥 = 𝐴 ) → ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → 𝐴 = 𝐵 ) )
41 40 com12 ⊢ ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) → 𝑥 = 𝐴 ) → 𝐴 = 𝐵 ) )
42 32 41 syld ⊢ ( ( 𝑥 = 𝐵 ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) )
43 42 ex ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) ) )
44 24 43 jaoi ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) ) )
45 44 com12 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) ) )
46 45 impd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) ) → 𝐴 = 𝐵 ) )
47 46 rexlimdva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ 𝑉 ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 = 𝑦 ) ) → 𝐴 = 𝐵 ) )
48 4 47 syl5bi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝐴 = 𝐵 ) )
49 reueq ⊢ ( 𝐵 ∈ 𝑉 ↔ ∃! 𝑥 ∈ 𝑉 𝑥 = 𝐵 )
50 49 biimpi ⊢ ( 𝐵 ∈ 𝑉 → ∃! 𝑥 ∈ 𝑉 𝑥 = 𝐵 )
51 50 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ∃! 𝑥 ∈ 𝑉 𝑥 = 𝐵 )
52 51 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = 𝐵 ) → ∃! 𝑥 ∈ 𝑉 𝑥 = 𝐵 )
53 eqeq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ↔ 𝑥 = 𝐵 ) )
54 53 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = 𝐵 ) → ( 𝑥 = 𝐴 ↔ 𝑥 = 𝐵 ) )
55 54 orbi1d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = 𝐵 ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( 𝑥 = 𝐵 ∨ 𝑥 = 𝐵 ) ) )
56 oridm ⊢ ( ( 𝑥 = 𝐵 ∨ 𝑥 = 𝐵 ) ↔ 𝑥 = 𝐵 )
57 55 56 bitrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = 𝐵 ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ 𝑥 = 𝐵 ) )
58 57 reubidv ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = 𝐵 ) → ( ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∃! 𝑥 ∈ 𝑉 𝑥 = 𝐵 ) )
59 52 58 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = 𝐵 ) → ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
60 59 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 = 𝐵 → ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
61 48 60 impbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∃! 𝑥 ∈ 𝑉 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ 𝐴 = 𝐵 ) )