Step | Hyp | Ref
| Expression |
1 | | relxp 5543 |
. 2
⊢ Rel
({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) |
2 | | relopabv 5665 |
. 2
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
3 | | df-clab 2717 |
. . . . 5
⊢ (𝑎 ∈ {𝑥 ∣ 𝜑} ↔ [𝑎 / 𝑥]𝜑) |
4 | | df-clab 2717 |
. . . . 5
⊢ (𝑏 ∈ {𝑦 ∣ 𝜓} ↔ [𝑏 / 𝑦]𝜓) |
5 | 3, 4 | anbi12i 630 |
. . . 4
⊢ ((𝑎 ∈ {𝑥 ∣ 𝜑} ∧ 𝑏 ∈ {𝑦 ∣ 𝜓}) ↔ ([𝑎 / 𝑥]𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
6 | | sban 2090 |
. . . . . . 7
⊢ ([𝑏 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑏 / 𝑦]𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
7 | | sbsbc 3684 |
. . . . . . 7
⊢ ([𝑏 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑏 / 𝑦](𝜑 ∧ 𝜓)) |
8 | | sbv 2098 |
. . . . . . . 8
⊢ ([𝑏 / 𝑦]𝜑 ↔ 𝜑) |
9 | 8 | anbi1i 627 |
. . . . . . 7
⊢ (([𝑏 / 𝑦]𝜑 ∧ [𝑏 / 𝑦]𝜓) ↔ (𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
10 | 6, 7, 9 | 3bitr3i 304 |
. . . . . 6
⊢
([𝑏 / 𝑦](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
11 | 10 | sbbii 2086 |
. . . . 5
⊢ ([𝑎 / 𝑥][𝑏 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑎 / 𝑥](𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
12 | | sbsbc 3684 |
. . . . 5
⊢ ([𝑎 / 𝑥][𝑏 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑦](𝜑 ∧ 𝜓)) |
13 | | sban 2090 |
. . . . . 6
⊢ ([𝑎 / 𝑥](𝜑 ∧ [𝑏 / 𝑦]𝜓) ↔ ([𝑎 / 𝑥]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑦]𝜓)) |
14 | | sbv 2098 |
. . . . . . 7
⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑏 / 𝑦]𝜓) |
15 | 14 | anbi2i 626 |
. . . . . 6
⊢ (([𝑎 / 𝑥]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑦]𝜓) ↔ ([𝑎 / 𝑥]𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
16 | 13, 15 | bitri 278 |
. . . . 5
⊢ ([𝑎 / 𝑥](𝜑 ∧ [𝑏 / 𝑦]𝜓) ↔ ([𝑎 / 𝑥]𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
17 | 11, 12, 16 | 3bitr3i 304 |
. . . 4
⊢
([𝑎 / 𝑥][𝑏 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑎 / 𝑥]𝜑 ∧ [𝑏 / 𝑦]𝜓)) |
18 | 5, 17 | bitr4i 281 |
. . 3
⊢ ((𝑎 ∈ {𝑥 ∣ 𝜑} ∧ 𝑏 ∈ {𝑦 ∣ 𝜓}) ↔ [𝑎 / 𝑥][𝑏 / 𝑦](𝜑 ∧ 𝜓)) |
19 | | brxp 5572 |
. . 3
⊢ (𝑎({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓})𝑏 ↔ (𝑎 ∈ {𝑥 ∣ 𝜑} ∧ 𝑏 ∈ {𝑦 ∣ 𝜓})) |
20 | | eqid 2738 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
21 | 20 | brabsb 5386 |
. . 3
⊢ (𝑎{〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)}𝑏 ↔ [𝑎 / 𝑥][𝑏 / 𝑦](𝜑 ∧ 𝜓)) |
22 | 18, 19, 21 | 3bitr4i 306 |
. 2
⊢ (𝑎({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓})𝑏 ↔ 𝑎{〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)}𝑏) |
23 | 1, 2, 22 | eqbrriv 5635 |
1
⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |