Proof of Theorem eqsbc3rVD
Step | Hyp | Ref
| Expression |
1 | | idn1 40906 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
2 | | eqsbc3 3816 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) |
3 | 1, 2 | e1a 40959 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) ) |
4 | | eqcom 2828 |
. . . . . . . . . 10
⊢ (𝐶 = 𝑥 ↔ 𝑥 = 𝐶) |
5 | 4 | sbcbii 3828 |
. . . . . . . . 9
⊢
([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶)) |
7 | 1, 6 | e1a 40959 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) ) |
8 | | idn2 40945 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ [𝐴 / 𝑥]𝐶 = 𝑥 ) |
9 | | biimp 217 |
. . . . . . 7
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) → ([𝐴 / 𝑥]𝐶 = 𝑥 → [𝐴 / 𝑥]𝑥 = 𝐶)) |
10 | 7, 8, 9 | e12 41056 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ [𝐴 / 𝑥]𝑥 = 𝐶 ) |
11 | | biimp 217 |
. . . . . 6
⊢
(([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) → ([𝐴 / 𝑥]𝑥 = 𝐶 → 𝐴 = 𝐶)) |
12 | 3, 10, 11 | e12 41056 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ 𝐴 = 𝐶 ) |
13 | | eqcom 2828 |
. . . . 5
⊢ (𝐴 = 𝐶 ↔ 𝐶 = 𝐴) |
14 | 12, 13 | e2bi 40964 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 , [𝐴 / 𝑥]𝐶 = 𝑥 ▶ 𝐶 = 𝐴 ) |
15 | 14 | in2 40937 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 → 𝐶 = 𝐴) ) |
16 | | idn2 40945 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ 𝐶 = 𝐴 ) |
17 | 16, 13 | e2bir 40965 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ 𝐴 = 𝐶 ) |
18 | | biimpr 222 |
. . . . . 6
⊢
(([𝐴 / 𝑥]𝑥 = 𝐶 ↔ 𝐴 = 𝐶) → (𝐴 = 𝐶 → [𝐴 / 𝑥]𝑥 = 𝐶)) |
19 | 3, 17, 18 | e12 41056 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ [𝐴 / 𝑥]𝑥 = 𝐶 ) |
20 | | biimpr 222 |
. . . . 5
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 ↔ [𝐴 / 𝑥]𝑥 = 𝐶) → ([𝐴 / 𝑥]𝑥 = 𝐶 → [𝐴 / 𝑥]𝐶 = 𝑥)) |
21 | 7, 19, 20 | e12 41056 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 , 𝐶 = 𝐴 ▶ [𝐴 / 𝑥]𝐶 = 𝑥 ) |
22 | 21 | in2 40937 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ (𝐶 = 𝐴 → [𝐴 / 𝑥]𝐶 = 𝑥) ) |
23 | | impbi 210 |
. . 3
⊢
(([𝐴 / 𝑥]𝐶 = 𝑥 → 𝐶 = 𝐴) → ((𝐶 = 𝐴 → [𝐴 / 𝑥]𝐶 = 𝑥) → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴))) |
24 | 15, 22, 23 | e11 41020 |
. 2
⊢ ( 𝐴 ∈ 𝐵 ▶ ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴) ) |
25 | 24 | in1 40903 |
1
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) |