Step | Hyp | Ref
| Expression |
1 | | nfsbc1v 3714 |
. . 3
⊢
Ⅎ𝑥[𝑐 / 𝑥]𝜑 |
2 | | nfsbc1v 3714 |
. . 3
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
3 | | sbceq1a 3705 |
. . 3
⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
4 | | dfsbcq 3696 |
. . 3
⊢ (𝑤 = 𝑐 → ([𝑤 / 𝑥]𝜑 ↔ [𝑐 / 𝑥]𝜑)) |
5 | 1, 2, 3, 4 | reu8nf 3789 |
. 2
⊢
(∃!𝑥 ∈
{𝐴, 𝐵}𝜑 ↔ ∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐))) |
6 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑥𝜓 |
7 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥{𝐴, 𝐵} |
8 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 = 𝑐 |
9 | 1, 8 | nfim 1904 |
. . . . . 6
⊢
Ⅎ𝑥([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) |
10 | 7, 9 | nfralw 3147 |
. . . . 5
⊢
Ⅎ𝑥∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) |
11 | 6, 10 | nfan 1907 |
. . . 4
⊢
Ⅎ𝑥(𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) |
12 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑥𝜒 |
13 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐵 = 𝑐 |
14 | 1, 13 | nfim 1904 |
. . . . . 6
⊢
Ⅎ𝑥([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐) |
15 | 7, 14 | nfralw 3147 |
. . . . 5
⊢
Ⅎ𝑥∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐) |
16 | 12, 15 | nfan 1907 |
. . . 4
⊢
Ⅎ𝑥(𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐)) |
17 | | reuprg.1 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
18 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑐 ↔ 𝐴 = 𝑐)) |
19 | 18 | imbi2d 344 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐))) |
20 | 19 | ralbidv 3118 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐))) |
21 | 17, 20 | anbi12d 634 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ (𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)))) |
22 | | reuprg.2 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
23 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 = 𝑐 ↔ 𝐵 = 𝑐)) |
24 | 23 | imbi2d 344 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐))) |
25 | 24 | ralbidv 3118 |
. . . . 5
⊢ (𝑥 = 𝐵 → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐))) |
26 | 22, 25 | anbi12d 634 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐)))) |
27 | 11, 16, 21, 26 | rexprgf 4609 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ ((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) ∨ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐))))) |
28 | | dfsbcq 3696 |
. . . . . . . 8
⊢ (𝑐 = 𝐴 → ([𝑐 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
29 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑐 = 𝐴 → (𝐴 = 𝑐 ↔ 𝐴 = 𝐴)) |
30 | 28, 29 | imbi12d 348 |
. . . . . . 7
⊢ (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴))) |
31 | | dfsbcq 3696 |
. . . . . . . 8
⊢ (𝑐 = 𝐵 → ([𝑐 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
32 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑐 = 𝐵 → (𝐴 = 𝑐 ↔ 𝐴 = 𝐵)) |
33 | 31, 32 | imbi12d 348 |
. . . . . . 7
⊢ (𝑐 = 𝐵 → (([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) ↔ ([𝐵 / 𝑥]𝜑 → 𝐴 = 𝐵))) |
34 | 30, 33 | ralprg 4610 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) ↔ (([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑 → 𝐴 = 𝐵)))) |
35 | | eqidd 2738 |
. . . . . . . 8
⊢
([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴) |
36 | 35 | biantrur 534 |
. . . . . . 7
⊢
(([𝐵 / 𝑥]𝜑 → 𝐴 = 𝐵) ↔ (([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑 → 𝐴 = 𝐵))) |
37 | 22 | sbcieg 3734 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑊 → ([𝐵 / 𝑥]𝜑 ↔ 𝜒)) |
38 | 37 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐵 / 𝑥]𝜑 ↔ 𝜒)) |
39 | 38 | imbi1d 345 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐵 / 𝑥]𝜑 → 𝐴 = 𝐵) ↔ (𝜒 → 𝐴 = 𝐵))) |
40 | 36, 39 | bitr3id 288 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑 → 𝐴 = 𝐵)) ↔ (𝜒 → 𝐴 = 𝐵))) |
41 | 34, 40 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) ↔ (𝜒 → 𝐴 = 𝐵))) |
42 | 41 | anbi2d 632 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) ↔ (𝜓 ∧ (𝜒 → 𝐴 = 𝐵)))) |
43 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑐 = 𝐴 → (𝐵 = 𝑐 ↔ 𝐵 = 𝐴)) |
44 | 28, 43 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑 → 𝐵 = 𝐴))) |
45 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑐 = 𝐵 → (𝐵 = 𝑐 ↔ 𝐵 = 𝐵)) |
46 | 31, 45 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑐 = 𝐵 → (([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐) ↔ ([𝐵 / 𝑥]𝜑 → 𝐵 = 𝐵))) |
47 | 44, 46 | ralprg 4610 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐) ↔ (([𝐴 / 𝑥]𝜑 → 𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑 → 𝐵 = 𝐵)))) |
48 | | eqidd 2738 |
. . . . . . . . 9
⊢
([𝐵 / 𝑥]𝜑 → 𝐵 = 𝐵) |
49 | 48 | biantru 533 |
. . . . . . . 8
⊢
(([𝐴 / 𝑥]𝜑 → 𝐵 = 𝐴) ↔ (([𝐴 / 𝑥]𝜑 → 𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑 → 𝐵 = 𝐵))) |
50 | 17 | sbcieg 3734 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
51 | 50 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
52 | 51 | imbi1d 345 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴 / 𝑥]𝜑 → 𝐵 = 𝐴) ↔ (𝜓 → 𝐵 = 𝐴))) |
53 | 49, 52 | bitr3id 288 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((([𝐴 / 𝑥]𝜑 → 𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑 → 𝐵 = 𝐵)) ↔ (𝜓 → 𝐵 = 𝐴))) |
54 | 47, 53 | bitrd 282 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐) ↔ (𝜓 → 𝐵 = 𝐴))) |
55 | 54 | anbi2d 632 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐)) ↔ (𝜒 ∧ (𝜓 → 𝐵 = 𝐴)))) |
56 | | eqcom 2744 |
. . . . . . 7
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
57 | 56 | imbi2i 339 |
. . . . . 6
⊢ ((𝜓 → 𝐵 = 𝐴) ↔ (𝜓 → 𝐴 = 𝐵)) |
58 | 57 | anbi2i 626 |
. . . . 5
⊢ ((𝜒 ∧ (𝜓 → 𝐵 = 𝐴)) ↔ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))) |
59 | 55, 58 | bitrdi 290 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐)) ↔ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵)))) |
60 | 42, 59 | orbi12d 919 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) ∨ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝐵 = 𝑐))) ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))))) |
61 | 27, 60 | bitrd 282 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))))) |
62 | 5, 61 | syl5bb 286 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))))) |