Step | Hyp | Ref
| Expression |
1 | | csbeq1 3754 |
. . . 4
⊢ (𝑧 = 𝐴 → ⦋𝑧 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑)) |
2 | | dfsbcq2 3655 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
3 | 2 | riotabidv 6885 |
. . . 4
⊢ (𝑧 = 𝐴 → (℩𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
4 | 1, 3 | eqeq12d 2793 |
. . 3
⊢ (𝑧 = 𝐴 → (⦋𝑧 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) ↔ ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))) |
5 | | vex 3401 |
. . . 4
⊢ 𝑧 ∈ V |
6 | | nfs1v 2254 |
. . . . 5
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
7 | | nfcv 2934 |
. . . . 5
⊢
Ⅎ𝑥𝐵 |
8 | 6, 7 | nfriota 6892 |
. . . 4
⊢
Ⅎ𝑥(℩𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
9 | | sbequ12 2229 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
10 | 9 | riotabidv 6885 |
. . . 4
⊢ (𝑥 = 𝑧 → (℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)) |
11 | 5, 8, 10 | csbief 3776 |
. . 3
⊢
⦋𝑧 /
𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
12 | 4, 11 | vtoclg 3467 |
. 2
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
13 | | csbprc 4206 |
. . 3
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = ∅) |
14 | | df-riota 6883 |
. . . 4
⊢
(℩𝑦
∈ 𝐵 [𝐴 / 𝑥]𝜑) = (℩𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑)) |
15 | | euex 2597 |
. . . . . . 7
⊢
(∃!𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑)) |
16 | | sbcex 3662 |
. . . . . . . . 9
⊢
([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
17 | 16 | adantl 475 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 ∈ V) |
18 | 17 | exlimiv 1973 |
. . . . . . 7
⊢
(∃𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 ∈ V) |
19 | 15, 18 | syl 17 |
. . . . . 6
⊢
(∃!𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → 𝐴 ∈ V) |
20 | 19 | con3i 152 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
∃!𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑)) |
21 | | iotanul 6114 |
. . . . 5
⊢ (¬
∃!𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → (℩𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑)) = ∅) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(℩𝑦(𝑦 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑)) = ∅) |
23 | 14, 22 | syl5req 2827 |
. . 3
⊢ (¬
𝐴 ∈ V → ∅ =
(℩𝑦 ∈
𝐵 [𝐴 / 𝑥]𝜑)) |
24 | 13, 23 | eqtrd 2814 |
. 2
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
25 | 12, 24 | pm2.61i 177 |
1
⊢
⦋𝐴 /
𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) |