Step | Hyp | Ref
| Expression |
1 | | anandir 802 |
. . . . . 6
⊢ (((xAa ∧ xBb) ∧ x ∈ C) ↔ ((xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C))) |
2 | 1 | anbi2i 675 |
. . . . 5
⊢ ((y = 〈a, b〉 ∧ ((xAa ∧ xBb) ∧ x ∈ C)) ↔ (y =
〈a,
b〉 ∧ ((xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C)))) |
3 | | 3anass 938 |
. . . . . . 7
⊢ ((y = 〈a, b〉 ∧ xAa ∧ xBb) ↔ (y =
〈a,
b〉 ∧ (xAa ∧ xBb))) |
4 | 3 | anbi1i 676 |
. . . . . 6
⊢ (((y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C) ↔ ((y =
〈a,
b〉 ∧ (xAa ∧ xBb)) ∧ x ∈ C)) |
5 | | anass 630 |
. . . . . 6
⊢ (((y = 〈a, b〉 ∧ (xAa ∧ xBb)) ∧ x ∈ C) ↔ (y =
〈a,
b〉 ∧ ((xAa ∧ xBb) ∧ x ∈ C))) |
6 | 4, 5 | bitri 240 |
. . . . 5
⊢ (((y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C) ↔ (y =
〈a,
b〉 ∧ ((xAa ∧ xBb) ∧ x ∈ C))) |
7 | | 3anass 938 |
. . . . 5
⊢ ((y = 〈a, b〉 ∧ (xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C)) ↔ (y =
〈a,
b〉 ∧ ((xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C)))) |
8 | 2, 6, 7 | 3bitr4i 268 |
. . . 4
⊢ (((y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C) ↔ (y =
〈a,
b〉 ∧ (xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C))) |
9 | 8 | 2exbii 1583 |
. . 3
⊢ (∃a∃b((y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C) ↔ ∃a∃b(y = 〈a, b〉 ∧ (xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C))) |
10 | | brtxp 5783 |
. . . . 5
⊢ (x(A ⊗
B)y
↔ ∃a∃b(y = 〈a, b〉 ∧ xAa ∧ xBb)) |
11 | 10 | anbi1i 676 |
. . . 4
⊢ ((x(A ⊗
B)y
∧ x ∈ C) ↔
(∃a∃b(y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C)) |
12 | | brres 4949 |
. . . 4
⊢ (x((A ⊗
B) ↾
C)y
↔ (x(A ⊗ B)y ∧ x ∈ C)) |
13 | | 19.41vv 1902 |
. . . 4
⊢ (∃a∃b((y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C) ↔ (∃a∃b(y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C)) |
14 | 11, 12, 13 | 3bitr4i 268 |
. . 3
⊢ (x((A ⊗
B) ↾
C)y
↔ ∃a∃b((y = 〈a, b〉 ∧ xAa ∧ xBb) ∧ x ∈ C)) |
15 | | brtxp 5783 |
. . . 4
⊢ (x((A ↾ C) ⊗
(B ↾
C))y
↔ ∃a∃b(y = 〈a, b〉 ∧ x(A ↾ C)a ∧ x(B ↾ C)b)) |
16 | | biid 227 |
. . . . . 6
⊢ (y = 〈a, b〉 ↔ y =
〈a,
b〉) |
17 | | brres 4949 |
. . . . . 6
⊢ (x(A ↾ C)a ↔ (xAa ∧ x ∈ C)) |
18 | | brres 4949 |
. . . . . 6
⊢ (x(B ↾ C)b ↔ (xBb ∧ x ∈ C)) |
19 | 16, 17, 18 | 3anbi123i 1140 |
. . . . 5
⊢ ((y = 〈a, b〉 ∧ x(A ↾ C)a ∧ x(B ↾ C)b) ↔ (y =
〈a,
b〉 ∧ (xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C))) |
20 | 19 | 2exbii 1583 |
. . . 4
⊢ (∃a∃b(y = 〈a, b〉 ∧ x(A ↾ C)a ∧ x(B ↾ C)b) ↔ ∃a∃b(y = 〈a, b〉 ∧ (xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C))) |
21 | 15, 20 | bitri 240 |
. . 3
⊢ (x((A ↾ C) ⊗
(B ↾
C))y
↔ ∃a∃b(y = 〈a, b〉 ∧ (xAa ∧ x ∈ C) ∧ (xBb ∧ x ∈ C))) |
22 | 9, 14, 21 | 3bitr4i 268 |
. 2
⊢ (x((A ⊗
B) ↾
C)y
↔ x((A ↾ C) ⊗ (B
↾ C))y) |
23 | 22 | eqbrriv 4851 |
1
⊢ ((A ⊗ B)
↾ C) =
((A ↾
C) ⊗ (B ↾ C)) |