| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-oprab 7436 | . . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)} | 
| 2 |  | rexcom4 3287 | . . . . 5
⊢
(∃𝑤 ∈
𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑤 ∈ 𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) | 
| 3 |  | rexcom4 3287 | . . . . . . 7
⊢
(∃𝑤 ∈
𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑦∃𝑤 ∈ 𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) | 
| 4 |  | rexcom4 3287 | . . . . . . . . 9
⊢
(∃𝑤 ∈
𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧∃𝑤 ∈ 𝐴 (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) | 
| 5 |  | r19.42v 3190 | . . . . . . . . . 10
⊢
(∃𝑤 ∈
𝐴 (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) | 
| 6 | 5 | exbii 1847 | . . . . . . . . 9
⊢
(∃𝑧∃𝑤 ∈ 𝐴 (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) | 
| 7 | 4, 6 | bitri 275 | . . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) | 
| 8 | 7 | exbii 1847 | . . . . . . 7
⊢
(∃𝑦∃𝑤 ∈ 𝐴 ∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) | 
| 9 | 3, 8 | bitri 275 | . . . . . 6
⊢
(∃𝑤 ∈
𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) | 
| 10 | 9 | exbii 1847 | . . . . 5
⊢
(∃𝑥∃𝑤 ∈ 𝐴 ∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)) | 
| 11 | 2, 10 | bitr2i 276 | . . . 4
⊢
(∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑) ↔ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) | 
| 12 | 11 | abbii 2808 | . . 3
⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ∃𝑤 ∈ 𝐴 𝜑)} = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} | 
| 13 | 1, 12 | eqtri 2764 | . 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} | 
| 14 |  | oprabrexex2.1 | . . 3
⊢ 𝐴 ∈ V | 
| 15 |  | df-oprab 7436 | . . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} | 
| 16 |  | oprabrexex2.2 | . . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V | 
| 17 | 15, 16 | eqeltrri 2837 | . . 3
⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ∈ V | 
| 18 | 14, 17 | abrexex2 7995 | . 2
⊢ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ∈ V | 
| 19 | 13, 18 | eqeltri 2836 | 1
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V |