| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. . . . 5
⊢
(([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴) |
| 2 | | nfsbc1v 3808 |
. . . . . . . 8
⊢
Ⅎ𝑦[𝐴 / 𝑦][𝐴 / 𝑥]𝜑 |
| 3 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑦[𝐴 / 𝑥]𝜑 |
| 4 | 2, 3 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑦([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) |
| 5 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑦 𝐴 = 𝐴 |
| 6 | 4, 5 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑦(([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴) |
| 7 | | sbceq1a 3799 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦][𝐴 / 𝑥]𝜑)) |
| 8 | | dfsbcq2 3791 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| 9 | 7, 8 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑))) |
| 10 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝐴 = 𝑦 ↔ 𝐴 = 𝐴)) |
| 11 | 9, 10 | imbi12d 344 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) ↔ (([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴))) |
| 12 | 6, 11 | ralsngf 4673 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) ↔ (([𝐴 / 𝑦][𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 = 𝐴))) |
| 13 | 1, 12 | mpbiri 258 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦)) |
| 14 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥{𝐴} |
| 15 | | nfsbc1v 3808 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
| 16 | | nfs1v 2156 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
| 17 | 15, 16 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑥([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) |
| 18 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 = 𝑦 |
| 19 | 17, 18 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑥(([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) |
| 20 | 14, 19 | nfralw 3311 |
. . . . 5
⊢
Ⅎ𝑥∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦) |
| 21 | | sbceq1a 3799 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| 22 | 21 | anbi1d 631 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑))) |
| 23 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑦 ↔ 𝐴 = 𝑦)) |
| 24 | 22, 23 | imbi12d 344 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦))) |
| 25 | 24 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦))) |
| 26 | 20, 25 | ralsngf 4673 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {𝐴} (([𝐴 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝐴 = 𝑦))) |
| 27 | 13, 26 | mpbird 257 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
| 28 | 27 | biantrud 531 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ (∃𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))) |
| 29 | | reu2 3731 |
. 2
⊢
(∃!𝑥 ∈
{𝐴}𝜑 ↔ (∃𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
| 30 | 28, 29 | bitr4di 289 |
1
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑)) |