Step | Hyp | Ref
| Expression |
1 | | df-oprab 6553 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)} |
2 | | rexcom4 3198 |
. . . . 5
⊢
(∃𝑤 ∈
𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑤 ∈ 𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
3 | | rexcom4 3198 |
. . . . . . 7
⊢
(∃𝑤 ∈
𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑦∃𝑤 ∈ 𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
4 | | rexcom4 3198 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧∃𝑤 ∈ 𝐴 (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
5 | | r19.42v 3073 |
. . . . . . . . . 10
⊢
(∃𝑤 ∈
𝐴 (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) |
6 | 5 | exbii 1764 |
. . . . . . . . 9
⊢
(∃𝑧∃𝑤 ∈ 𝐴 (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) |
7 | 4, 6 | bitri 263 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) |
8 | 7 | exbii 1764 |
. . . . . . 7
⊢
(∃𝑦∃𝑤 ∈ 𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) |
9 | 3, 8 | bitri 263 |
. . . . . 6
⊢
(∃𝑤 ∈
𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) |
10 | 9 | exbii 1764 |
. . . . 5
⊢
(∃𝑥∃𝑤 ∈ 𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) |
11 | 2, 10 | bitr2i 264 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑) ↔ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
12 | 11 | abbii 2726 |
. . 3
⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)} = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
13 | 1, 12 | eqtri 2632 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
14 | | oprabrexex2.1 |
. . 3
⊢ 𝐴 ∈ V |
15 | | df-oprab 6553 |
. . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
16 | | oprabrexex2.2 |
. . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V |
17 | 15, 16 | eqeltrri 2685 |
. . 3
⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ∈ V |
18 | 14, 17 | abrexex2 7040 |
. 2
⊢ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ∈ V |
19 | 13, 18 | eqeltri 2684 |
1
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V |