| Step | Hyp | Ref
| Expression |
| 1 | | 19.42v 1953 |
. . . . . . 7
⊢
(∃𝑥(𝑦 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐴 ∧ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
| 2 | | an12 645 |
. . . . . . . 8
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
| 3 | 2 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
| 4 | | elxp 5708 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦}))) |
| 5 | | ancom 460 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦}) ↔ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
| 6 | 5 | anbi2i 623 |
. . . . . . . . . . 11
⊢ ((𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦})) ↔ (𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 7 | 6 | 2exbii 1849 |
. . . . . . . . . 10
⊢
(∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦})) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 8 | 4, 7 | bitri 275 |
. . . . . . . . 9
⊢ (𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 9 | | an12 645 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑣 ∈ {𝑦} ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 10 | | velsn 4642 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑦} ↔ 𝑣 = 𝑦) |
| 11 | 10 | anbi1i 624 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ {𝑦} ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 12 | 9, 11 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 13 | 12 | exbii 1848 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ ∃𝑣(𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 14 | | opeq2 4874 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → 〈𝑤, 𝑣〉 = 〈𝑤, 𝑦〉) |
| 15 | 14 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → (𝑧 = 〈𝑤, 𝑣〉 ↔ 𝑧 = 〈𝑤, 𝑦〉)) |
| 16 | 15 | anbi1d 631 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑦 → ((𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
| 17 | 16 | equsexvw 2004 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
| 18 | 13, 17 | bitri 275 |
. . . . . . . . . 10
⊢
(∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
| 19 | 18 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ ∃𝑤(𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
| 20 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑧 = 〈𝑤, 𝑦〉 |
| 21 | | nfsab1 2722 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 ∈ {𝑥 ∣ 𝜓} |
| 22 | 20, 21 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) |
| 23 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑤(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) |
| 24 | | opeq1 4873 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → 〈𝑤, 𝑦〉 = 〈𝑥, 𝑦〉) |
| 25 | 24 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑧 = 〈𝑤, 𝑦〉 ↔ 𝑧 = 〈𝑥, 𝑦〉)) |
| 26 | | df-clab 2715 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑥 ∣ 𝜓} ↔ [𝑤 / 𝑥]𝜓) |
| 27 | | sbequ12 2251 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑥]𝜓)) |
| 28 | 27 | equcoms 2019 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝜓 ↔ [𝑤 / 𝑥]𝜓)) |
| 29 | 26, 28 | bitr4id 290 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑤 ∈ {𝑥 ∣ 𝜓} ↔ 𝜓)) |
| 30 | 25, 29 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → ((𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
| 31 | 22, 23, 30 | cbvexv1 2344 |
. . . . . . . . 9
⊢
(∃𝑤(𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
| 32 | 8, 19, 31 | 3bitri 297 |
. . . . . . . 8
⊢ (𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
| 33 | 32 | anbi2i 623 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ (𝑦 ∈ 𝐴 ∧ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
| 34 | 1, 3, 33 | 3bitr4ri 304 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 35 | 34 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ ∃𝑦∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 36 | | excom 2162 |
. . . . 5
⊢
(∃𝑦∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 37 | 35, 36 | bitri 275 |
. . . 4
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 38 | | eliun 4995 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) |
| 39 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}))) |
| 40 | 38, 39 | bitri 275 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}))) |
| 41 | | elopab 5532 |
. . . 4
⊢ (𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 42 | 37, 40, 41 | 3bitr4i 303 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ↔ 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}) |
| 43 | 42 | eqriv 2734 |
. 2
⊢ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) = {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
| 44 | | opabex3rd.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 45 | | opabex3rd.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → {𝑥 ∣ 𝜓} ∈ V) |
| 46 | | vsnex 5434 |
. . . . 5
⊢ {𝑦} ∈ V |
| 47 | | xpexg 7770 |
. . . . 5
⊢ (({𝑥 ∣ 𝜓} ∈ V ∧ {𝑦} ∈ V) → ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
| 48 | 45, 46, 47 | sylancl 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
| 49 | 48 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
| 50 | | iunexg 7988 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) → ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
| 51 | 44, 49, 50 | syl2anc 584 |
. 2
⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
| 52 | 43, 51 | eqeltrrid 2846 |
1
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ∈ V) |