Step | Hyp | Ref
| Expression |
1 | | cbvrald.nf0 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑧𝜑 |
3 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑧 𝑥 ∈ 𝐴 |
4 | 3 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑧 𝑥 ∈ 𝐴) |
5 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑧𝜓 |
6 | 5 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑧𝜓) |
7 | 4, 6 | nfimd 1578 |
. . . 4
⊢ (𝜑 → Ⅎ𝑧(𝑥 ∈ 𝐴 → 𝜓)) |
8 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
9 | 8 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑥 𝑧 ∈ 𝐴) |
10 | | nfs1v 1932 |
. . . . . 6
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜓 |
11 | 10 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑥[𝑧 / 𝑥]𝜓) |
12 | 9, 11 | nfimd 1578 |
. . . 4
⊢ (𝜑 → Ⅎ𝑥(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓)) |
13 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
14 | 13 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
15 | | sbequ12 1764 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑥]𝜓)) |
16 | 15 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ [𝑧 / 𝑥]𝜓)) |
17 | 14, 16 | imbi12d 233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓))) |
18 | 17 | ex 114 |
. . . 4
⊢ (𝜑 → (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓)))) |
19 | 1, 2, 7, 12, 18 | cbv2 1742 |
. . 3
⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓))) |
20 | | cbvrald.nf1 |
. . . 4
⊢
Ⅎ𝑦𝜑 |
21 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑦 𝑧 ∈ 𝐴 |
22 | 21 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑦 𝑧 ∈ 𝐴) |
23 | | cbvrald.nf2 |
. . . . . 6
⊢ (𝜑 → Ⅎ𝑦𝜓) |
24 | 1, 23 | nfsbd 1970 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑦[𝑧 / 𝑥]𝜓) |
25 | 22, 24 | nfimd 1578 |
. . . 4
⊢ (𝜑 → Ⅎ𝑦(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓)) |
26 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑧 𝑦 ∈ 𝐴 |
27 | 26 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑧 𝑦 ∈ 𝐴) |
28 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑧𝜒 |
29 | 28 | a1i 9 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑧𝜒) |
30 | 27, 29 | nfimd 1578 |
. . . 4
⊢ (𝜑 → Ⅎ𝑧(𝑦 ∈ 𝐴 → 𝜒)) |
31 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
32 | 31 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑦) → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
33 | | sbequ 1833 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓)) |
34 | | cbvrald.nf3 |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥𝜒) |
35 | | cbvrald.is |
. . . . . . . 8
⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) |
36 | 1, 34, 35 | sbied 1781 |
. . . . . . 7
⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) |
37 | 33, 36 | sylan9bbr 460 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝑦) → ([𝑧 / 𝑥]𝜓 ↔ 𝜒)) |
38 | 32, 37 | imbi12d 233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 𝑦) → ((𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓) ↔ (𝑦 ∈ 𝐴 → 𝜒))) |
39 | 38 | ex 114 |
. . . 4
⊢ (𝜑 → (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓) ↔ (𝑦 ∈ 𝐴 → 𝜒)))) |
40 | 2, 20, 25, 30, 39 | cbv2 1742 |
. . 3
⊢ (𝜑 → (∀𝑧(𝑧 ∈ 𝐴 → [𝑧 / 𝑥]𝜓) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜒))) |
41 | 19, 40 | bitrd 187 |
. 2
⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜒))) |
42 | | df-ral 2453 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
43 | | df-ral 2453 |
. 2
⊢
(∀𝑦 ∈
𝐴 𝜒 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜒)) |
44 | 41, 42, 43 | 3bitr4g 222 |
1
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒)) |