Proof of Theorem resoprab2
Step | Hyp | Ref
| Expression |
1 | | resoprab 5539 |
. 2
⊢
({〈〈x, y〉, z〉
∣ ((x ∈ A ∧ y ∈ B) ∧ φ)}
↾ (𝐶 × 𝐷)) = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧
((x ∈
A ∧
y ∈
B) ∧ φ))} |
2 | | anass 381 |
. . . 4
⊢
((((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ (x ∈ A ∧ y ∈ B)) ∧ φ) ↔
((x ∈
𝐶 ∧ y ∈ 𝐷) ∧
((x ∈
A ∧
y ∈
B) ∧ φ))) |
3 | | an4 520 |
. . . . . 6
⊢
(((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ (x ∈ A ∧ y ∈ B)) ↔
((x ∈
𝐶 ∧ x ∈ A) ∧ (y ∈ 𝐷 ∧ y ∈ B))) |
4 | | ssel 2933 |
. . . . . . . . 9
⊢ (𝐶 ⊆ A → (x
∈ 𝐶 → x ∈ A)) |
5 | 4 | pm4.71d 373 |
. . . . . . . 8
⊢ (𝐶 ⊆ A → (x
∈ 𝐶 ↔ (x ∈ 𝐶 ∧ x ∈ A))) |
6 | 5 | bicomd 129 |
. . . . . . 7
⊢ (𝐶 ⊆ A → ((x
∈ 𝐶 ∧ x ∈ A) ↔ x
∈ 𝐶)) |
7 | | ssel 2933 |
. . . . . . . . 9
⊢ (𝐷 ⊆ B → (y
∈ 𝐷 → y ∈ B)) |
8 | 7 | pm4.71d 373 |
. . . . . . . 8
⊢ (𝐷 ⊆ B → (y
∈ 𝐷 ↔ (y ∈ 𝐷 ∧ y ∈ B))) |
9 | 8 | bicomd 129 |
. . . . . . 7
⊢ (𝐷 ⊆ B → ((y
∈ 𝐷 ∧ y ∈ B) ↔ y
∈ 𝐷)) |
10 | 6, 9 | bi2anan9 538 |
. . . . . 6
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → (((x
∈ 𝐶 ∧ x ∈ A) ∧ (y ∈ 𝐷 ∧ y ∈ B)) ↔
(x ∈
𝐶 ∧ y ∈ 𝐷))) |
11 | 3, 10 | syl5bb 181 |
. . . . 5
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → (((x
∈ 𝐶 ∧ y ∈ 𝐷) ∧ (x ∈ A ∧ y ∈ B)) ↔
(x ∈
𝐶 ∧ y ∈ 𝐷))) |
12 | 11 | anbi1d 438 |
. . . 4
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ((((x
∈ 𝐶 ∧ y ∈ 𝐷) ∧ (x ∈ A ∧ y ∈ B)) ∧ φ) ↔
((x ∈
𝐶 ∧ y ∈ 𝐷) ∧ φ))) |
13 | 2, 12 | syl5bbr 183 |
. . 3
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → (((x
∈ 𝐶 ∧ y ∈ 𝐷) ∧ ((x ∈ A ∧ y ∈ B) ∧ φ)) ↔
((x ∈
𝐶 ∧ y ∈ 𝐷) ∧ φ))) |
14 | 13 | oprabbidv 5501 |
. 2
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧
((x ∈
A ∧
y ∈
B) ∧ φ))} = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)}) |
15 | 1, 14 | syl5eq 2081 |
1
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ({〈〈x, y〉,
z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ↾ (𝐶 × 𝐷)) = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)}) |