| Step | Hyp | Ref
| Expression |
| 1 | | nfsbc1v 3808 |
. . 3
⊢
Ⅎ𝑥[𝑐 / 𝑥]𝜑 |
| 2 | | nfsbc1v 3808 |
. . 3
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
| 3 | | sbceq1a 3799 |
. . 3
⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
| 4 | | dfsbcq 3790 |
. . 3
⊢ (𝑤 = 𝑐 → ([𝑤 / 𝑥]𝜑 ↔ [𝑐 / 𝑥]𝜑)) |
| 5 | 1, 2, 3, 4 | reu8nf 3877 |
. 2
⊢
(∃!𝑥 ∈
{𝐴}𝜑 ↔ ∃𝑥 ∈ {𝐴} (𝜑 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐))) |
| 6 | | rexsngf.1 |
. . . . 5
⊢
Ⅎ𝑥𝜓 |
| 7 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥{𝐴} |
| 8 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 = 𝑐 |
| 9 | 1, 8 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑥([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) |
| 10 | 7, 9 | nfralw 3311 |
. . . . 5
⊢
Ⅎ𝑥∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) |
| 11 | 6, 10 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑥(𝜓 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) |
| 12 | | rexsngf.2 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| 13 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑐 ↔ 𝐴 = 𝑐)) |
| 14 | 13 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐))) |
| 15 | 14 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐))) |
| 16 | 12, 15 | anbi12d 632 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ (𝜓 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)))) |
| 17 | 11, 16 | rexsngf 4672 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴} (𝜑 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ (𝜓 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)))) |
| 18 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑐([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴) |
| 19 | | dfsbcq 3790 |
. . . . . . 7
⊢ (𝑐 = 𝐴 → ([𝑐 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| 20 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑐 = 𝐴 → (𝐴 = 𝑐 ↔ 𝐴 = 𝐴)) |
| 21 | 19, 20 | imbi12d 344 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴))) |
| 22 | 18, 21 | ralsngf 4673 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴))) |
| 23 | 22 | anbi2d 630 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝜓 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) ↔ (𝜓 ∧ ([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴)))) |
| 24 | | eqidd 2738 |
. . . . 5
⊢
([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴) |
| 25 | 24 | biantru 529 |
. . . 4
⊢ (𝜓 ↔ (𝜓 ∧ ([𝐴 / 𝑥]𝜑 → 𝐴 = 𝐴))) |
| 26 | 23, 25 | bitr4di 289 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((𝜓 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝐴 = 𝑐)) ↔ 𝜓)) |
| 27 | 17, 26 | bitrd 279 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴} (𝜑 ∧ ∀𝑐 ∈ {𝐴} ([𝑐 / 𝑥]𝜑 → 𝑥 = 𝑐)) ↔ 𝜓)) |
| 28 | 5, 27 | bitrid 283 |
1
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |