Proof of Theorem eqsbc3rVD
Step | Hyp | Ref
| Expression |
1 | | idn1 38790 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
2 | | eqsbc3 3475 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) |
3 | 1, 2 | e1a 38852 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) ) |
4 | | eqcom 2629 |
. . . . . . . . 9
⊢ (𝐶 = 𝑥 ↔ 𝑥 = 𝐶) |
5 | 4 | sbcbiiOLD 38741 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶)) |
6 | 1, 5 | e1a 38852 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) ) |
7 | | idn2 38838 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ [𝐴 / 𝑥]𝐶 = 𝑥 ) |
8 | | biimp 205 |
. . . . . . 7
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) → ([𝐴 / 𝑥]𝐶 = 𝑥 → [𝐴 / 𝑥]𝑥 = 𝐶)) |
9 | 6, 7, 8 | e12 38951 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ [𝐴 / 𝑥]𝑥 = 𝐶 ) |
10 | | biimp 205 |
. . . . . 6
⊢
(([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) → ([𝐴 / 𝑥]𝑥 = 𝐶 → 𝐴 = 𝐶)) |
11 | 3, 9, 10 | e12 38951 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ 𝐴 = 𝐶 ) |
12 | | eqcom 2629 |
. . . . 5
⊢ (𝐴 = 𝐶 ↔ 𝐶 = 𝐴) |
13 | 11, 12 | e2bi 38857 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ 𝐶 = 𝐴 ) |
14 | 13 | in2 38830 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 → 𝐶 = 𝐴) ) |
15 | | idn2 38838 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ 𝐶 = 𝐴 ) |
16 | 15, 12 | e2bir 38858 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ 𝐴 = 𝐶 ) |
17 | | biimpr 210 |
. . . . . 6
⊢
(([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) → (𝐴 = 𝐶 → [𝐴 / 𝑥]𝑥 = 𝐶)) |
18 | 3, 16, 17 | e12 38951 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ [𝐴 / 𝑥]𝑥 = 𝐶 ) |
19 | | biimpr 210 |
. . . . 5
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) → ([𝐴 / 𝑥]𝑥 = 𝐶 → [𝐴 / 𝑥]𝐶 = 𝑥)) |
20 | 6, 18, 19 | e12 38951 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ [𝐴 / 𝑥]𝐶 = 𝑥 ) |
21 | 20 | in2 38830 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ (𝐶 = 𝐴 → [𝐴 / 𝑥]𝐶 = 𝑥) ) |
22 | | impbi 198 |
. . 3
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 → 𝐶 = 𝐴) → ((𝐶 = 𝐴 → [𝐴 / 𝑥]𝐶 = 𝑥) → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴))) |
23 | 14, 21, 22 | e11 38913 |
. 2
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴) ) |
24 | 23 | in1 38787 |
1
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) |