Proof of Theorem sbcne12
Step | Hyp | Ref
| Expression |
1 | | nne 2786 |
. . . . . 6
⊢ (¬
𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶) |
2 | 1 | sbcbii 3458 |
. . . . 5
⊢
([𝐴 / 𝑥] ¬ 𝐵 ≠ 𝐶 ↔ [𝐴 / 𝑥]𝐵 = 𝐶) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥] ¬ 𝐵 ≠ 𝐶 ↔ [𝐴 / 𝑥]𝐵 = 𝐶)) |
4 | | sbcng 3443 |
. . . 4
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥] ¬ 𝐵 ≠ 𝐶 ↔ ¬ [𝐴 / 𝑥]𝐵 ≠ 𝐶)) |
5 | | sbceqg 3936 |
. . . . 5
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
6 | | nne 2786 |
. . . . 5
⊢ (¬
⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
7 | 5, 6 | syl6bbr 277 |
. . . 4
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ¬ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)) |
8 | 3, 4, 7 | 3bitr3d 297 |
. . 3
⊢ (𝐴 ∈ V → (¬
[𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ¬ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)) |
9 | 8 | con4bid 306 |
. 2
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)) |
10 | | sbcex 3412 |
. . . 4
⊢
([𝐴 / 𝑥]𝐵 ≠ 𝐶 → 𝐴 ∈ V) |
11 | 10 | con3i 149 |
. . 3
⊢ (¬
𝐴 ∈ V → ¬
[𝐴 / 𝑥]𝐵 ≠ 𝐶) |
12 | | csbprc 3932 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐵 = ∅) |
13 | | csbprc 3932 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐶 = ∅) |
14 | 12, 13 | eqtr4d 2647 |
. . . 4
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
15 | 14, 6 | sylibr 223 |
. . 3
⊢ (¬
𝐴 ∈ V → ¬
⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶) |
16 | 11, 15 | 2falsed 365 |
. 2
⊢ (¬
𝐴 ∈ V →
([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)) |
17 | 9, 16 | pm2.61i 175 |
1
⊢
([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶) |