Proof of Theorem csbie2df
Step | Hyp | Ref
| Expression |
1 | | csbie2df.a |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | eqidd 2741 |
. . 3
⊢ (𝜑 → 𝐷 = 𝐷) |
3 | | dfsbcq 3722 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝐵 = 𝐷 ↔ [𝐴 / 𝑥]𝐵 = 𝐷)) |
4 | | sbceqg 4349 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐷)) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → ([𝐴 / 𝑥]𝐵 = 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐷)) |
6 | | csbie2df.d |
. . . . . . . . . 10
⊢ (𝜑 → Ⅎ𝑥𝐷) |
7 | | csbtt 3854 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐷) → ⦋𝐴 / 𝑥⦌𝐷 = 𝐷) |
8 | 6, 7 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → ⦋𝐴 / 𝑥⦌𝐷 = 𝐷) |
9 | 8 | eqeq2d 2751 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → (⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)) |
10 | 5, 9 | bitrd 278 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → ([𝐴 / 𝑥]𝐵 = 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)) |
11 | 1, 10 | mpancom 685 |
. . . . . 6
⊢ (𝜑 → ([𝐴 / 𝑥]𝐵 = 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)) |
12 | 3, 11 | sylan9bb 510 |
. . . . 5
⊢ ((𝑦 = 𝐴 ∧ 𝜑) → ([𝑦 / 𝑥]𝐵 = 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)) |
13 | 12 | pm5.74da 801 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝜑 → [𝑦 / 𝑥]𝐵 = 𝐷) ↔ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷))) |
14 | | csbie2df.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐶 = 𝐷) |
15 | 14 | eqeq1d 2742 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → (𝐶 = 𝐷 ↔ 𝐷 = 𝐷)) |
16 | 15 | expcom 414 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝜑 → (𝐶 = 𝐷 ↔ 𝐷 = 𝐷))) |
17 | 16 | pm5.74d 272 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝜑 → 𝐶 = 𝐷) ↔ (𝜑 → 𝐷 = 𝐷))) |
18 | | sbsbc 3724 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝐵 = 𝐷 ↔ [𝑦 / 𝑥]𝐵 = 𝐷) |
19 | | csbie2df.p |
. . . . . . 7
⊢
Ⅎ𝑥𝜑 |
20 | | csbie2df.c |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥𝐶) |
21 | 20, 6 | nfeqd 2919 |
. . . . . . 7
⊢ (𝜑 → Ⅎ𝑥 𝐶 = 𝐷) |
22 | | csbie2df.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) |
23 | 22 | eqeq1d 2742 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝐵 = 𝐷 ↔ 𝐶 = 𝐷)) |
24 | 23 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (𝑥 = 𝑦 → (𝐵 = 𝐷 ↔ 𝐶 = 𝐷))) |
25 | 19, 21, 24 | sbiedw 2314 |
. . . . . 6
⊢ (𝜑 → ([𝑦 / 𝑥]𝐵 = 𝐷 ↔ 𝐶 = 𝐷)) |
26 | 18, 25 | bitr3id 285 |
. . . . 5
⊢ (𝜑 → ([𝑦 / 𝑥]𝐵 = 𝐷 ↔ 𝐶 = 𝐷)) |
27 | 26 | pm5.74i 270 |
. . . 4
⊢ ((𝜑 → [𝑦 / 𝑥]𝐵 = 𝐷) ↔ (𝜑 → 𝐶 = 𝐷)) |
28 | 13, 17, 27 | vtoclbg 3506 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) ↔ (𝜑 → 𝐷 = 𝐷))) |
29 | 2, 28 | mpbiri 257 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)) |
30 | 1, 29 | mpcom 38 |
1
⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) |