Step | Hyp | Ref
| Expression |
1 | | opsbc2ie.a |
. . . . . . . . 9
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒)) |
2 | 1 | sbcth 3784 |
. . . . . . . 8
⊢ (𝑥 ∈ V → [𝑥 / 𝑎](𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))) |
3 | | sbcim1 3825 |
. . . . . . . 8
⊢
([𝑥 / 𝑎](𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒)) → ([𝑥 / 𝑎]𝑝 = ⟨𝑎, 𝑏⟩ → [𝑥 / 𝑎](𝜑 ↔ 𝜒))) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ V → ([𝑥 / 𝑎]𝑝 = ⟨𝑎, 𝑏⟩ → [𝑥 / 𝑎](𝜑 ↔ 𝜒))) |
5 | | sbceq2g 4408 |
. . . . . . . 8
⊢ (𝑥 ∈ V → ([𝑥 / 𝑎]𝑝 = ⟨𝑎, 𝑏⟩ ↔ 𝑝 = ⦋𝑥 / 𝑎⦌⟨𝑎, 𝑏⟩)) |
6 | | csbopg 4883 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V →
⦋𝑥 / 𝑎⦌⟨𝑎, 𝑏⟩ = ⟨⦋𝑥 / 𝑎⦌𝑎, ⦋𝑥 / 𝑎⦌𝑏⟩) |
7 | | csbvarg 4423 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ V →
⦋𝑥 / 𝑎⦌𝑎 = 𝑥) |
8 | | csbconstg 3904 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ V →
⦋𝑥 / 𝑎⦌𝑏 = 𝑏) |
9 | 7, 8 | opeq12d 4873 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V →
⟨⦋𝑥 /
𝑎⦌𝑎, ⦋𝑥 / 𝑎⦌𝑏⟩ = ⟨𝑥, 𝑏⟩) |
10 | 6, 9 | eqtrd 2764 |
. . . . . . . . 9
⊢ (𝑥 ∈ V →
⦋𝑥 / 𝑎⦌⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑏⟩) |
11 | 10 | eqeq2d 2735 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑝 = ⦋𝑥 / 𝑎⦌⟨𝑎, 𝑏⟩ ↔ 𝑝 = ⟨𝑥, 𝑏⟩)) |
12 | 5, 11 | bitrd 279 |
. . . . . . 7
⊢ (𝑥 ∈ V → ([𝑥 / 𝑎]𝑝 = ⟨𝑎, 𝑏⟩ ↔ 𝑝 = ⟨𝑥, 𝑏⟩)) |
13 | | sbcbig 3823 |
. . . . . . . 8
⊢ (𝑥 ∈ V → ([𝑥 / 𝑎](𝜑 ↔ 𝜒) ↔ ([𝑥 / 𝑎]𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
14 | | sbcg 3848 |
. . . . . . . . 9
⊢ (𝑥 ∈ V → ([𝑥 / 𝑎]𝜑 ↔ 𝜑)) |
15 | 14 | bibi1d 343 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (([𝑥 / 𝑎]𝜑 ↔ [𝑥 / 𝑎]𝜒) ↔ (𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
16 | 13, 15 | bitrd 279 |
. . . . . . 7
⊢ (𝑥 ∈ V → ([𝑥 / 𝑎](𝜑 ↔ 𝜒) ↔ (𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
17 | 4, 12, 16 | 3imtr3d 293 |
. . . . . 6
⊢ (𝑥 ∈ V → (𝑝 = ⟨𝑥, 𝑏⟩ → (𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
18 | 17 | elv 3472 |
. . . . 5
⊢ (𝑝 = ⟨𝑥, 𝑏⟩ → (𝜑 ↔ [𝑥 / 𝑎]𝜒)) |
19 | 18 | sbcth 3784 |
. . . 4
⊢ (𝑦 ∈ V → [𝑦 / 𝑏](𝑝 = ⟨𝑥, 𝑏⟩ → (𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
20 | | sbcim1 3825 |
. . . 4
⊢
([𝑦 / 𝑏](𝑝 = ⟨𝑥, 𝑏⟩ → (𝜑 ↔ [𝑥 / 𝑎]𝜒)) → ([𝑦 / 𝑏]𝑝 = ⟨𝑥, 𝑏⟩ → [𝑦 / 𝑏](𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (𝑦 ∈ V → ([𝑦 / 𝑏]𝑝 = ⟨𝑥, 𝑏⟩ → [𝑦 / 𝑏](𝜑 ↔ [𝑥 / 𝑎]𝜒))) |
22 | | sbceq2g 4408 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑏]𝑝 = ⟨𝑥, 𝑏⟩ ↔ 𝑝 = ⦋𝑦 / 𝑏⦌⟨𝑥, 𝑏⟩)) |
23 | | csbopg 4883 |
. . . . . 6
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑏⦌⟨𝑥, 𝑏⟩ = ⟨⦋𝑦 / 𝑏⦌𝑥, ⦋𝑦 / 𝑏⦌𝑏⟩) |
24 | | csbconstg 3904 |
. . . . . . 7
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑏⦌𝑥 = 𝑥) |
25 | | csbvarg 4423 |
. . . . . . 7
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑏⦌𝑏 = 𝑦) |
26 | 24, 25 | opeq12d 4873 |
. . . . . 6
⊢ (𝑦 ∈ V →
⟨⦋𝑦 /
𝑏⦌𝑥, ⦋𝑦 / 𝑏⦌𝑏⟩ = ⟨𝑥, 𝑦⟩) |
27 | 23, 26 | eqtrd 2764 |
. . . . 5
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑏⦌⟨𝑥, 𝑏⟩ = ⟨𝑥, 𝑦⟩) |
28 | 27 | eqeq2d 2735 |
. . . 4
⊢ (𝑦 ∈ V → (𝑝 = ⦋𝑦 / 𝑏⦌⟨𝑥, 𝑏⟩ ↔ 𝑝 = ⟨𝑥, 𝑦⟩)) |
29 | 22, 28 | bitrd 279 |
. . 3
⊢ (𝑦 ∈ V → ([𝑦 / 𝑏]𝑝 = ⟨𝑥, 𝑏⟩ ↔ 𝑝 = ⟨𝑥, 𝑦⟩)) |
30 | | sbcbig 3823 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑏](𝜑 ↔ [𝑥 / 𝑎]𝜒) ↔ ([𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))) |
31 | | sbcg 3848 |
. . . . 5
⊢ (𝑦 ∈ V → ([𝑦 / 𝑏]𝜑 ↔ 𝜑)) |
32 | 31 | bibi1d 343 |
. . . 4
⊢ (𝑦 ∈ V → (([𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒) ↔ (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))) |
33 | 30, 32 | bitrd 279 |
. . 3
⊢ (𝑦 ∈ V → ([𝑦 / 𝑏](𝜑 ↔ [𝑥 / 𝑎]𝜒) ↔ (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))) |
34 | 21, 29, 33 | 3imtr3d 293 |
. 2
⊢ (𝑦 ∈ V → (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))) |
35 | 34 | elv 3472 |
1
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)) |