Step | Hyp | Ref
| Expression |
1 | | nfv 1916 |
. . . 4
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 → 𝜑) |
2 | | cbvralfwOLD.1 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
3 | 2 | nfcri 2904 |
. . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | | nfs1v 2158 |
. . . . 5
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
5 | 3, 4 | nfim 1898 |
. . . 4
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) |
6 | | eleq1w 2833 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
7 | | sbequ12 2251 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
8 | 6, 7 | imbi12d 349 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbvalv1 2351 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑)) |
10 | | cbvralfwOLD.2 |
. . . . . 6
⊢
Ⅎ𝑦𝐴 |
11 | 10 | nfcri 2904 |
. . . . 5
⊢
Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | | cbvralfwOLD.3 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
13 | 12 | nfsbv 2339 |
. . . . 5
⊢
Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfim 1898 |
. . . 4
⊢
Ⅎ𝑦(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) |
15 | | nfv 1916 |
. . . 4
⊢
Ⅎ𝑧(𝑦 ∈ 𝐴 → 𝜓) |
16 | | eleq1w 2833 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
17 | | sbequ 2089 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
18 | | cbvralfwOLD.4 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
19 | | cbvralfwOLD.5 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
20 | 18, 19 | sbiev 2323 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | bitrdi 290 |
. . . . 5
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | imbi12d 349 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
23 | 14, 15, 22 | cbvalv1 2351 |
. . 3
⊢
(∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
24 | 9, 23 | bitri 278 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
25 | | df-ral 3073 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
26 | | df-ral 3073 |
. 2
⊢
(∀𝑦 ∈
𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
27 | 24, 25, 26 | 3bitr4i 307 |
1
⊢
(∀𝑥 ∈
𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |