Step | Hyp | Ref
| Expression |
1 | | nfv 1920 |
. . . 4
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 → 𝜑) |
2 | | cbvralfwOLD.1 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
3 | 2 | nfcri 2895 |
. . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | | nfs1v 2156 |
. . . . 5
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
5 | 3, 4 | nfim 1902 |
. . . 4
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) |
6 | | eleq1w 2822 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
7 | | sbequ12 2247 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
8 | 6, 7 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbvalv1 2341 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑)) |
10 | | cbvralfwOLD.2 |
. . . . . 6
⊢
Ⅎ𝑦𝐴 |
11 | 10 | nfcri 2895 |
. . . . 5
⊢
Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | | cbvralfwOLD.3 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
13 | 12 | nfsbv 2327 |
. . . . 5
⊢
Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfim 1902 |
. . . 4
⊢
Ⅎ𝑦(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) |
15 | | nfv 1920 |
. . . 4
⊢
Ⅎ𝑧(𝑦 ∈ 𝐴 → 𝜓) |
16 | | eleq1w 2822 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
17 | | sbequ 2089 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
18 | | cbvralfwOLD.4 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
19 | | cbvralfwOLD.5 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
20 | 18, 19 | sbiev 2312 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | bitrdi 286 |
. . . . 5
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | imbi12d 344 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
23 | 14, 15, 22 | cbvalv1 2341 |
. . 3
⊢
(∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
24 | 9, 23 | bitri 274 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
25 | | df-ral 3070 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
26 | | df-ral 3070 |
. 2
⊢
(∀𝑦 ∈
𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
27 | 24, 25, 26 | 3bitr4i 302 |
1
⊢
(∀𝑥 ∈
𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |