Proof of Theorem csbopg
| Step | Hyp | Ref
| Expression |
| 1 | | csbif 4583 |
. . 3
⊢
⦋𝐴 /
𝑥⦌if((𝐶 ∈ V ∧ 𝐷 ∈ V), {{𝐶}, {𝐶, 𝐷}}, ∅) = if([𝐴 / 𝑥](𝐶 ∈ V ∧ 𝐷 ∈ V), ⦋𝐴 / 𝑥⦌{{𝐶}, {𝐶, 𝐷}}, ⦋𝐴 / 𝑥⦌∅) |
| 2 | | sbcan 3838 |
. . . . 5
⊢
([𝐴 / 𝑥](𝐶 ∈ V ∧ 𝐷 ∈ V) ↔ ([𝐴 / 𝑥]𝐶 ∈ V ∧ [𝐴 / 𝑥]𝐷 ∈ V)) |
| 3 | | sbcel1g 4416 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐶 ∈ V ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ V)) |
| 4 | | sbcel1g 4416 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐷 ∈ V ↔ ⦋𝐴 / 𝑥⦌𝐷 ∈ V)) |
| 5 | 3, 4 | anbi12d 632 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝐶 ∈ V ∧ [𝐴 / 𝑥]𝐷 ∈ V) ↔ (⦋𝐴 / 𝑥⦌𝐶 ∈ V ∧ ⦋𝐴 / 𝑥⦌𝐷 ∈ V))) |
| 6 | 2, 5 | bitrid 283 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝐶 ∈ V ∧ 𝐷 ∈ V) ↔ (⦋𝐴 / 𝑥⦌𝐶 ∈ V ∧ ⦋𝐴 / 𝑥⦌𝐷 ∈ V))) |
| 7 | | csbprg 4709 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{{𝐶}, {𝐶, 𝐷}} = {⦋𝐴 / 𝑥⦌{𝐶}, ⦋𝐴 / 𝑥⦌{𝐶, 𝐷}}) |
| 8 | | csbsng 4708 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐶} = {⦋𝐴 / 𝑥⦌𝐶}) |
| 9 | | csbprg 4709 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐶, 𝐷} = {⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷}) |
| 10 | 8, 9 | preq12d 4741 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → {⦋𝐴 / 𝑥⦌{𝐶}, ⦋𝐴 / 𝑥⦌{𝐶, 𝐷}} = {{⦋𝐴 / 𝑥⦌𝐶}, {⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷}}) |
| 11 | 7, 10 | eqtrd 2777 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{{𝐶}, {𝐶, 𝐷}} = {{⦋𝐴 / 𝑥⦌𝐶}, {⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷}}) |
| 12 | | csbconstg 3918 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∅ =
∅) |
| 13 | 6, 11, 12 | ifbieq12d 4554 |
. . 3
⊢ (𝐴 ∈ 𝑉 → if([𝐴 / 𝑥](𝐶 ∈ V ∧ 𝐷 ∈ V), ⦋𝐴 / 𝑥⦌{{𝐶}, {𝐶, 𝐷}}, ⦋𝐴 / 𝑥⦌∅) =
if((⦋𝐴 /
𝑥⦌𝐶 ∈ V ∧
⦋𝐴 / 𝑥⦌𝐷 ∈ V), {{⦋𝐴 / 𝑥⦌𝐶}, {⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷}}, ∅)) |
| 14 | 1, 13 | eqtrid 2789 |
. 2
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌if((𝐶 ∈ V ∧ 𝐷 ∈ V), {{𝐶}, {𝐶, 𝐷}}, ∅) = if((⦋𝐴 / 𝑥⦌𝐶 ∈ V ∧ ⦋𝐴 / 𝑥⦌𝐷 ∈ V), {{⦋𝐴 / 𝑥⦌𝐶}, {⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷}}, ∅)) |
| 15 | | dfopif 4870 |
. . 3
⊢
〈𝐶, 𝐷〉 = if((𝐶 ∈ V ∧ 𝐷 ∈ V), {{𝐶}, {𝐶, 𝐷}}, ∅) |
| 16 | 15 | csbeq2i 3907 |
. 2
⊢
⦋𝐴 /
𝑥⦌〈𝐶, 𝐷〉 = ⦋𝐴 / 𝑥⦌if((𝐶 ∈ V ∧ 𝐷 ∈ V), {{𝐶}, {𝐶, 𝐷}}, ∅) |
| 17 | | dfopif 4870 |
. 2
⊢
〈⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷〉 = if((⦋𝐴 / 𝑥⦌𝐶 ∈ V ∧ ⦋𝐴 / 𝑥⦌𝐷 ∈ V), {{⦋𝐴 / 𝑥⦌𝐶}, {⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷}}, ∅) |
| 18 | 14, 16, 17 | 3eqtr4g 2802 |
1
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝐶, 𝐷〉 = 〈⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷〉) |