Proof of Theorem csbiebt
Step | Hyp | Ref
| Expression |
1 | | elex 3426 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | spsbc 3707 |
. . . . 5
⊢ (𝐴 ∈ V → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) → [𝐴 / 𝑥](𝑥 = 𝐴 → 𝐵 = 𝐶))) |
3 | 2 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) → [𝐴 / 𝑥](𝑥 = 𝐴 → 𝐵 = 𝐶))) |
4 | | simpl 486 |
. . . . 5
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → 𝐴 ∈ V) |
5 | | biimt 364 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐵 = 𝐶 ↔ (𝑥 = 𝐴 → 𝐵 = 𝐶))) |
6 | | csbeq1a 3825 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
7 | 6 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
8 | 5, 7 | bitr3d 284 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
9 | 8 | adantl 485 |
. . . . 5
⊢ (((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) ∧ 𝑥 = 𝐴) → ((𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
10 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑥 𝐴 ∈ V |
11 | | nfnfc1 2907 |
. . . . . 6
⊢
Ⅎ𝑥Ⅎ𝑥𝐶 |
12 | 10, 11 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑥(𝐴 ∈ V ∧
Ⅎ𝑥𝐶) |
13 | | nfcsb1v 3836 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
15 | | simpr 488 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → Ⅎ𝑥𝐶) |
16 | 14, 15 | nfeqd 2914 |
. . . . 5
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
17 | 4, 9, 12, 16 | sbciedf 3738 |
. . . 4
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → ([𝐴 / 𝑥](𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
18 | 3, 17 | sylibd 242 |
. . 3
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
19 | 13 | a1i 11 |
. . . . . . . 8
⊢
(Ⅎ𝑥𝐶 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
20 | | id 22 |
. . . . . . . 8
⊢
(Ⅎ𝑥𝐶 → Ⅎ𝑥𝐶) |
21 | 19, 20 | nfeqd 2914 |
. . . . . . 7
⊢
(Ⅎ𝑥𝐶 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
22 | 11, 21 | nfan1 2198 |
. . . . . 6
⊢
Ⅎ𝑥(Ⅎ𝑥𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
23 | 7 | biimprcd 253 |
. . . . . . 7
⊢
(⦋𝐴 /
𝑥⦌𝐵 = 𝐶 → (𝑥 = 𝐴 → 𝐵 = 𝐶)) |
24 | 23 | adantl 485 |
. . . . . 6
⊢
((Ⅎ𝑥𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) → (𝑥 = 𝐴 → 𝐵 = 𝐶)) |
25 | 22, 24 | alrimi 2211 |
. . . . 5
⊢
((Ⅎ𝑥𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) → ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶)) |
26 | 25 | ex 416 |
. . . 4
⊢
(Ⅎ𝑥𝐶 → (⦋𝐴 / 𝑥⦌𝐵 = 𝐶 → ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶))) |
27 | 26 | adantl 485 |
. . 3
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → (⦋𝐴 / 𝑥⦌𝐵 = 𝐶 → ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶))) |
28 | 18, 27 | impbid 215 |
. 2
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
29 | 1, 28 | sylan 583 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |