Proof of Theorem eqsbc3rVD
Step | Hyp | Ref
| Expression |
1 | | idn1 41867 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
2 | | eqsbc3 3743 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) |
3 | 1, 2 | e1a 41920 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) ) |
4 | | eqcom 2744 |
. . . . . . . . . 10
⊢ (𝐶 = 𝑥 ↔ 𝑥 = 𝐶) |
5 | 4 | sbcbii 3755 |
. . . . . . . . 9
⊢
([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶)) |
7 | 1, 6 | e1a 41920 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) ) |
8 | | idn2 41906 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ [𝐴 / 𝑥]𝐶 = 𝑥 ) |
9 | | biimp 218 |
. . . . . . 7
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) → ([𝐴 / 𝑥]𝐶 = 𝑥 → [𝐴 / 𝑥]𝑥 = 𝐶)) |
10 | 7, 8, 9 | e12 42017 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ [𝐴 / 𝑥]𝑥 = 𝐶 ) |
11 | | biimp 218 |
. . . . . 6
⊢
(([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) → ([𝐴 / 𝑥]𝑥 = 𝐶 → 𝐴 = 𝐶)) |
12 | 3, 10, 11 | e12 42017 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ 𝐴 = 𝐶 ) |
13 | | eqcom 2744 |
. . . . 5
⊢ (𝐴 = 𝐶 ↔ 𝐶 = 𝐴) |
14 | 12, 13 | e2bi 41925 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ 𝐶 = 𝐴 ) |
15 | 14 | in2 41898 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 → 𝐶 = 𝐴) ) |
16 | | idn2 41906 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ 𝐶 = 𝐴 ) |
17 | 16, 13 | e2bir 41926 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ 𝐴 = 𝐶 ) |
18 | | biimpr 223 |
. . . . . 6
⊢
(([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) → (𝐴 = 𝐶 → [𝐴 / 𝑥]𝑥 = 𝐶)) |
19 | 3, 17, 18 | e12 42017 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ [𝐴 / 𝑥]𝑥 = 𝐶 ) |
20 | | biimpr 223 |
. . . . 5
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) → ([𝐴 / 𝑥]𝑥 = 𝐶 → [𝐴 / 𝑥]𝐶 = 𝑥)) |
21 | 7, 19, 20 | e12 42017 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ [𝐴 / 𝑥]𝐶 = 𝑥 ) |
22 | 21 | in2 41898 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ (𝐶 = 𝐴 → [𝐴 / 𝑥]𝐶 = 𝑥) ) |
23 | | impbi 211 |
. . 3
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 → 𝐶 = 𝐴) → ((𝐶 = 𝐴 → [𝐴 / 𝑥]𝐶 = 𝑥) → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴))) |
24 | 15, 22, 23 | e11 41981 |
. 2
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴) ) |
25 | 24 | in1 41864 |
1
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) |