| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqeq1 2741 | . . . . . 6
⊢ (𝑧 = 𝑤 → (𝑧 = 〈𝑥, 𝑦〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) | 
| 2 | 1 | anbi1d 631 | . . . . 5
⊢ (𝑧 = 𝑤 → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | 
| 3 | 2 | 2exbidv 1924 | . . . 4
⊢ (𝑧 = 𝑤 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | 
| 4 | 1 | anbi1d 631 | . . . . 5
⊢ (𝑧 = 𝑤 → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 5 | 4 | 2exbidv 1924 | . . . 4
⊢ (𝑧 = 𝑤 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 6 | 3, 5 | unabw 4307 | . . 3
⊢ ({𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ∪ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)}) = {𝑤 ∣ (∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))} | 
| 7 |  | 19.43 1882 | . . . . 5
⊢
(∃𝑥(∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ (∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 8 |  | andi 1010 | . . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 9 | 8 | exbii 1848 | . . . . . . 7
⊢
(∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓)) ↔ ∃𝑦((𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 10 |  | 19.43 1882 | . . . . . . 7
⊢
(∃𝑦((𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ (∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 11 | 9, 10 | bitr2i 276 | . . . . . 6
⊢
((∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓))) | 
| 12 | 11 | exbii 1848 | . . . . 5
⊢
(∃𝑥(∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓))) | 
| 13 | 7, 12 | bitr3i 277 | . . . 4
⊢
((∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓))) | 
| 14 | 13 | abbii 2809 | . . 3
⊢ {𝑤 ∣ (∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑) ∨ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜓))} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓))} | 
| 15 | 6, 14 | eqtri 2765 | . 2
⊢ ({𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ∪ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)}) = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓))} | 
| 16 |  | df-opab 5206 | . . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | 
| 17 |  | df-opab 5206 | . . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)} | 
| 18 | 16, 17 | uneq12i 4166 | . 2
⊢
({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = ({𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ∪ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)}) | 
| 19 |  | df-opab 5206 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ (𝜑 ∨ 𝜓))} | 
| 20 | 15, 18, 19 | 3eqtr4i 2775 | 1
⊢
({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} |