Step | Hyp | Ref
| Expression |
1 | | eqidd 2741 |
. . . . 5
⊢
(([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴) |
2 | | nfsbc1v 3740 |
. . . . . . . 8
⊢
Ⅎ𝑦[𝐴 / 𝑦][𝐴 / 𝑥]𝜑 |
3 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑦[𝐴 / 𝑥]𝜑 |
4 | 2, 3 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑦([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) |
5 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑦 𝐴 = 𝐴 |
6 | 4, 5 | nfim 1903 |
. . . . . 6
⊢
Ⅎ𝑦(([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴) |
7 | | sbceq1a 3731 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦][𝐴 / 𝑥]𝜑)) |
8 | | dfsbcq2 3723 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
9 | 7, 8 | anbi12d 631 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑))) |
10 | | eqeq2 2752 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝐴 = 𝑦 ↔ 𝐴 = 𝐴)) |
11 | 9, 10 | imbi12d 345 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) ↔ (([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴))) |
12 | 6, 11 | ralsngf 4613 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) ↔ (([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴))) |
13 | 1, 12 | mpbiri 257 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦)) |
14 | | nfcv 2909 |
. . . . . 6
⊢
Ⅎ𝑥{𝐴} |
15 | | nfsbc1v 3740 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
16 | | nfs1v 2157 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
17 | 15, 16 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑥([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) |
18 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 = 𝑦 |
19 | 17, 18 | nfim 1903 |
. . . . . 6
⊢
Ⅎ𝑥(([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) |
20 | 14, 19 | nfralw 3152 |
. . . . 5
⊢
Ⅎ𝑥∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) |
21 | | sbceq1a 3731 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
22 | 21 | anbi1d 630 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑))) |
23 | | eqeq1 2744 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑦 ↔ 𝐴 = 𝑦)) |
24 | 22, 23 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦))) |
25 | 24 | ralbidv 3123 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦))) |
26 | 20, 25 | ralsngf 4613 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦))) |
27 | 13, 26 | mpbird 256 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
28 | 27 | biantrud 532 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ (∃𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))) |
29 | | reu2 3664 |
. 2
⊢
(∃!𝑥 ∈
{𝐴}𝜑 ↔ (∃𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
30 | 28, 29 | bitr4di 289 |
1
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑)) |