Proof of Theorem vtocl2d
Step | Hyp | Ref
| Expression |
1 | | vtocl2d.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
2 | | vtocl2d.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | nfcv 2934 |
. . . 4
⊢
Ⅎ𝑦𝐵 |
4 | | nfcv 2934 |
. . . 4
⊢
Ⅎ𝑥𝐵 |
5 | | nfcv 2934 |
. . . 4
⊢
Ⅎ𝑥𝐴 |
6 | | nfv 1957 |
. . . . 5
⊢
Ⅎ𝑦𝜑 |
7 | | nfsbc1v 3672 |
. . . . 5
⊢
Ⅎ𝑦[𝐵 / 𝑦]𝜓 |
8 | 6, 7 | nfim 1943 |
. . . 4
⊢
Ⅎ𝑦(𝜑 → [𝐵 / 𝑦]𝜓) |
9 | | nfv 1957 |
. . . 4
⊢
Ⅎ𝑥(𝜑 → 𝜒) |
10 | | sbceq1a 3663 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝜓 ↔ [𝐵 / 𝑦]𝜓)) |
11 | 10 | imbi2d 332 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝜑 → 𝜓) ↔ (𝜑 → [𝐵 / 𝑦]𝜓))) |
12 | | sbceq1a 3663 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ([𝐵 / 𝑦]𝜓 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜓)) |
13 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜒 |
14 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜒 |
15 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝐵 ∈ 𝑊 |
16 | | vtocl2d.1 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)) |
17 | 13, 14, 15, 16 | sbc2iegf 3722 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
18 | 2, 1, 17 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
19 | 12, 18 | sylan9bb 505 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝜑) → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
20 | 19 | pm5.74da 794 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝜑 → [𝐵 / 𝑦]𝜓) ↔ (𝜑 → 𝜒))) |
21 | | vtocl2d.3 |
. . . 4
⊢ (𝜑 → 𝜓) |
22 | 3, 4, 5, 8, 9, 11,
20, 21 | vtocl2gf 3469 |
. . 3
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (𝜑 → 𝜒)) |
23 | 1, 2, 22 | syl2anc 579 |
. 2
⊢ (𝜑 → (𝜑 → 𝜒)) |
24 | 23 | pm2.43i 52 |
1
⊢ (𝜑 → 𝜒) |