Step | Hyp | Ref
| Expression |
1 | | nfv 1508 |
. . . 4
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 → 𝜑) |
2 | | cbvralf.1 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
3 | 2 | nfcri 2293 |
. . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | | nfs1v 1919 |
. . . . 5
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
5 | 3, 4 | nfim 1552 |
. . . 4
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) |
6 | | eleq1 2220 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
7 | | sbequ12 1751 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
8 | 6, 7 | imbi12d 233 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbval 1734 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑)) |
10 | | cbvralf.2 |
. . . . . 6
⊢
Ⅎ𝑦𝐴 |
11 | 10 | nfcri 2293 |
. . . . 5
⊢
Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | | cbvralf.3 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
13 | 12 | nfsb 1926 |
. . . . 5
⊢
Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfim 1552 |
. . . 4
⊢
Ⅎ𝑦(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) |
15 | | nfv 1508 |
. . . 4
⊢
Ⅎ𝑧(𝑦 ∈ 𝐴 → 𝜓) |
16 | | eleq1 2220 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
17 | | sbequ 1820 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
18 | | cbvralf.4 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
19 | | cbvralf.5 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
20 | 18, 19 | sbie 1771 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | bitrdi 195 |
. . . . 5
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | imbi12d 233 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
23 | 14, 15, 22 | cbval 1734 |
. . 3
⊢
(∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
24 | 9, 23 | bitri 183 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
25 | | df-ral 2440 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
26 | | df-ral 2440 |
. 2
⊢
(∀𝑦 ∈
𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
27 | 24, 25, 26 | 3bitr4i 211 |
1
⊢
(∀𝑥 ∈
𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |