Step | Hyp | Ref
| Expression |
1 | | eqeq1 2742 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
2 | | eqeq1 2742 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐵 ↔ 𝑦 = 𝐵)) |
3 | 1, 2 | orbi12d 916 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵))) |
4 | 3 | reu8 3668 |
. . 3
⊢
(∃!𝑥 ∈
𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∃𝑥 ∈ 𝑉 ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦))) |
5 | | simprlr 777 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
6 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (𝑦 = 𝐴 ↔ 𝐵 = 𝐴)) |
7 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (𝑦 = 𝐵 ↔ 𝐵 = 𝐵)) |
8 | 6, 7 | orbi12d 916 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵))) |
9 | | eqeq2 2750 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐵)) |
10 | 8, 9 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → (((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐵 = 𝐴 ∨ 𝐵 = 𝐵) → 𝑥 = 𝐵))) |
11 | 10 | rspcv 3557 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴 ∨ 𝐵 = 𝐵) → 𝑥 = 𝐵))) |
12 | 5, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴 ∨ 𝐵 = 𝐵) → 𝑥 = 𝐵))) |
13 | | ioran 981 |
. . . . . . . . . . . 12
⊢ (¬
(𝐵 = 𝐴 ∨ 𝐵 = 𝐵) ↔ (¬ 𝐵 = 𝐴 ∧ ¬ 𝐵 = 𝐵)) |
14 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ 𝐵 = 𝐵 |
15 | 14 | pm2.24i 150 |
. . . . . . . . . . . 12
⊢ (¬
𝐵 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
16 | 13, 15 | simplbiim 505 |
. . . . . . . . . . 11
⊢ (¬
(𝐵 = 𝐴 ∨ 𝐵 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
17 | | eqtr2 2762 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → 𝐴 = 𝐵) |
18 | 17 | ancoms 459 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → 𝐴 = 𝐵) |
19 | 18 | a1d 25 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → 𝐴 = 𝐵)) |
20 | 19 | expimpd 454 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
21 | 16, 20 | ja 186 |
. . . . . . . . . 10
⊢ (((𝐵 = 𝐴 ∨ 𝐵 = 𝐵) → 𝑥 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
22 | 21 | com12 32 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → (((𝐵 = 𝐴 ∨ 𝐵 = 𝐵) → 𝑥 = 𝐵) → 𝐴 = 𝐵)) |
23 | 12, 22 | syld 47 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)) |
24 | 23 | ex 413 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))) |
25 | | simprll 776 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
26 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑦 = 𝐴 ↔ 𝐴 = 𝐴)) |
27 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑦 = 𝐵 ↔ 𝐴 = 𝐵)) |
28 | 26, 27 | orbi12d 916 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) |
29 | | eqeq2 2750 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴)) |
30 | 28, 29 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) → 𝑥 = 𝐴))) |
31 | 30 | rspcv 3557 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) → 𝑥 = 𝐴))) |
32 | 25, 31 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) → 𝑥 = 𝐴))) |
33 | | ioran 981 |
. . . . . . . . . . . 12
⊢ (¬
(𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ↔ (¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵)) |
34 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ 𝐴 = 𝐴 |
35 | 34 | pm2.24i 150 |
. . . . . . . . . . . . 13
⊢ (¬
𝐴 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
36 | 35 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((¬
𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
37 | 33, 36 | sylbi 216 |
. . . . . . . . . . 11
⊢ (¬
(𝐴 = 𝐴 ∨ 𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
38 | 17 | a1d 25 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → 𝐴 = 𝐵)) |
39 | 38 | expimpd 454 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
40 | 37, 39 | ja 186 |
. . . . . . . . . 10
⊢ (((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) → 𝑥 = 𝐴) → ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → 𝐴 = 𝐵)) |
41 | 40 | com12 32 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → (((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) → 𝑥 = 𝐴) → 𝐴 = 𝐵)) |
42 | 32, 41 | syld 47 |
. . . . . . . 8
⊢ ((𝑥 = 𝐵 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉)) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)) |
43 | 42 | ex 413 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))) |
44 | 24, 43 | jaoi 854 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))) |
45 | 44 | com12 32 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))) |
46 | 45 | impd 411 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵)) |
47 | 46 | rexlimdva 3213 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑉 ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵)) |
48 | 4, 47 | syl5bi 241 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝐴 = 𝐵)) |
49 | | reueq 3672 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑉 ↔ ∃!𝑥 ∈ 𝑉 𝑥 = 𝐵) |
50 | 49 | biimpi 215 |
. . . . . 6
⊢ (𝐵 ∈ 𝑉 → ∃!𝑥 ∈ 𝑉 𝑥 = 𝐵) |
51 | 50 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ∃!𝑥 ∈ 𝑉 𝑥 = 𝐵) |
52 | 51 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥 ∈ 𝑉 𝑥 = 𝐵) |
53 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) |
54 | 53 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = 𝐵) → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵)) |
55 | 54 | orbi1d 914 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ (𝑥 = 𝐵 ∨ 𝑥 = 𝐵))) |
56 | | oridm 902 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∨ 𝑥 = 𝐵) ↔ 𝑥 = 𝐵) |
57 | 55, 56 | bitrdi 287 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝑥 = 𝐵)) |
58 | 57 | reubidv 3323 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = 𝐵) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∃!𝑥 ∈ 𝑉 𝑥 = 𝐵)) |
59 | 52, 58 | mpbird 256 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
60 | 59 | ex 413 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 = 𝐵 → ∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
61 | 48, 60 | impbid 211 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵)) |