Step | Hyp | Ref
| Expression |
1 | | wl-dfrabsb 34876 |
. 2
⊢ {𝑥 : 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)} |
2 | | clelsb3 2940 |
. . . . . 6
⊢ ([𝑧 / 𝑦]𝑦 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) |
3 | | clelsb3 2940 |
. . . . . 6
⊢ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) |
4 | 2, 3 | bitr4i 280 |
. . . . 5
⊢ ([𝑧 / 𝑦]𝑦 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑥 ∈ 𝐴) |
5 | | sbco2vv 2108 |
. . . . 5
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑) |
6 | 4, 5 | anbi12i 628 |
. . . 4
⊢ (([𝑧 / 𝑦]𝑦 ∈ 𝐴 ∧ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)) |
7 | | df-clab 2800 |
. . . . 5
⊢ (𝑧 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)} ↔ [𝑧 / 𝑦](𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)) |
8 | | sban 2086 |
. . . . 5
⊢ ([𝑧 / 𝑦](𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑦]𝑦 ∈ 𝐴 ∧ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
9 | 7, 8 | bitri 277 |
. . . 4
⊢ (𝑧 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)} ↔ ([𝑧 / 𝑦]𝑦 ∈ 𝐴 ∧ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
10 | | df-clab 2800 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ [𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) |
11 | | sban 2086 |
. . . . 5
⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)) |
12 | 10, 11 | bitri 277 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)) |
13 | 6, 9, 12 | 3bitr4i 305 |
. . 3
⊢ (𝑧 ∈ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
14 | 13 | eqriv 2818 |
. 2
⊢ {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
15 | 1, 14 | eqtri 2844 |
1
⊢ {𝑥 : 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |