Step | Hyp | Ref
| Expression |
1 | | 19.42v 1961 |
. . . . . . 7
⊢
(∃𝑥(𝑦 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐴 ∧ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
2 | | an12 645 |
. . . . . . . 8
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
3 | 2 | exbii 1854 |
. . . . . . 7
⊢
(∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
4 | | elxp 5558 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦}))) |
5 | | ancom 464 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦}) ↔ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
6 | 5 | anbi2i 626 |
. . . . . . . . . . 11
⊢ ((𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦})) ↔ (𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
7 | 6 | 2exbii 1855 |
. . . . . . . . . 10
⊢
(∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ {𝑥 ∣ 𝜓} ∧ 𝑣 ∈ {𝑦})) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
8 | 4, 7 | bitri 278 |
. . . . . . . . 9
⊢ (𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
9 | | an12 645 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑣 ∈ {𝑦} ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
10 | | velsn 4542 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑦} ↔ 𝑣 = 𝑦) |
11 | 10 | anbi1i 627 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ {𝑦} ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
12 | 9, 11 | bitri 278 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
13 | 12 | exbii 1854 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ ∃𝑣(𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
14 | | opeq2 4771 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → 〈𝑤, 𝑣〉 = 〈𝑤, 𝑦〉) |
15 | 14 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → (𝑧 = 〈𝑤, 𝑣〉 ↔ 𝑧 = 〈𝑤, 𝑦〉)) |
16 | 15 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑦 → ((𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}))) |
17 | 16 | equsexvw 2016 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑣 = 𝑦 ∧ (𝑧 = 〈𝑤, 𝑣〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
18 | 13, 17 | bitri 278 |
. . . . . . . . . 10
⊢
(∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
19 | 18 | exbii 1854 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣(𝑧 = 〈𝑤, 𝑣〉 ∧ (𝑣 ∈ {𝑦} ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) ↔ ∃𝑤(𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓})) |
20 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑧 = 〈𝑤, 𝑦〉 |
21 | | nfsab1 2726 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 ∈ {𝑥 ∣ 𝜓} |
22 | 20, 21 | nfan 1906 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) |
23 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑤(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) |
24 | | opeq1 4769 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → 〈𝑤, 𝑦〉 = 〈𝑥, 𝑦〉) |
25 | 24 | eqeq2d 2750 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑧 = 〈𝑤, 𝑦〉 ↔ 𝑧 = 〈𝑥, 𝑦〉)) |
26 | | df-clab 2718 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑥 ∣ 𝜓} ↔ [𝑤 / 𝑥]𝜓) |
27 | | sbequ12 2253 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑥]𝜓)) |
28 | 27 | equcoms 2032 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝜓 ↔ [𝑤 / 𝑥]𝜓)) |
29 | 26, 28 | bitr4id 293 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝑤 ∈ {𝑥 ∣ 𝜓} ↔ 𝜓)) |
30 | 25, 29 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → ((𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
31 | 22, 23, 30 | cbvexv1 2345 |
. . . . . . . . 9
⊢
(∃𝑤(𝑧 = 〈𝑤, 𝑦〉 ∧ 𝑤 ∈ {𝑥 ∣ 𝜓}) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
32 | 8, 19, 31 | 3bitri 300 |
. . . . . . . 8
⊢ (𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
33 | 32 | anbi2i 626 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ (𝑦 ∈ 𝐴 ∧ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
34 | 1, 3, 33 | 3bitr4ri 307 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ ∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
35 | 34 | exbii 1854 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ ∃𝑦∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
36 | | excom 2170 |
. . . . 5
⊢
(∃𝑦∃𝑥(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
37 | 35, 36 | bitri 278 |
. . . 4
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
38 | | eliun 4895 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦})) |
39 | | df-rex 3060 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}))) |
40 | 38, 39 | bitri 278 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥 ∣ 𝜓} × {𝑦}))) |
41 | | elopab 5392 |
. . . 4
⊢ (𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
42 | 37, 40, 41 | 3bitr4i 306 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ↔ 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}) |
43 | 42 | eqriv 2736 |
. 2
⊢ ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) = {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
44 | | opabex3rd.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
45 | | opabex3rd.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → {𝑥 ∣ 𝜓} ∈ V) |
46 | | snex 5308 |
. . . . 5
⊢ {𝑦} ∈ V |
47 | | xpexg 7504 |
. . . . 5
⊢ (({𝑥 ∣ 𝜓} ∈ V ∧ {𝑦} ∈ V) → ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
48 | 45, 46, 47 | sylancl 589 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
49 | 48 | ralrimiva 3097 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
50 | | iunexg 7702 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) → ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
51 | 44, 49, 50 | syl2anc 587 |
. 2
⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ({𝑥 ∣ 𝜓} × {𝑦}) ∈ V) |
52 | 43, 51 | eqeltrrid 2839 |
1
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ∈ V) |