Step | Hyp | Ref
| Expression |
1 | | 19.42v 1893 |
. . . . . 6
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
2 | | an12 551 |
. . . . . . 7
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
3 | 2 | exbii 1592 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
4 | | elxp 4618 |
. . . . . . . 8
⊢ (𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑣∃𝑤(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
5 | | excom 1651 |
. . . . . . . . 9
⊢
(∃𝑣∃𝑤(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
6 | | an12 551 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑣 ∈ {𝑥} ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
7 | | velsn 3590 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑥} ↔ 𝑣 = 𝑥) |
8 | 7 | anbi1i 454 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ {𝑥} ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
9 | 6, 8 | bitri 183 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
10 | 9 | exbii 1592 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑣(𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
11 | | vex 2727 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | opeq1 3755 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑥 → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑤〉) |
13 | 12 | eqeq2d 2176 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑥 → (𝑧 = 〈𝑣, 𝑤〉 ↔ 𝑧 = 〈𝑥, 𝑤〉)) |
14 | 13 | anbi1d 461 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑥 → ((𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) ↔ (𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
15 | 11, 14 | ceqsexv 2763 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
16 | 10, 15 | bitri 183 |
. . . . . . . . . 10
⊢
(∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
17 | 16 | exbii 1592 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑤(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
18 | 5, 17 | bitri 183 |
. . . . . . . 8
⊢
(∃𝑣∃𝑤(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑤(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
19 | | nfv 1515 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑧 = 〈𝑥, 𝑤〉 |
20 | | nfsab1 2154 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑤 ∈ {𝑦 ∣ 𝜓} |
21 | 19, 20 | nfan 1552 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) |
22 | | nfv 1515 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) |
23 | | opeq2 3756 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → 〈𝑥, 𝑤〉 = 〈𝑥, 𝑦〉) |
24 | 23 | eqeq2d 2176 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑧 = 〈𝑥, 𝑤〉 ↔ 𝑧 = 〈𝑥, 𝑦〉)) |
25 | | df-clab 2151 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑦 ∣ 𝜓} ↔ [𝑤 / 𝑦]𝜓) |
26 | | sbequ12 1758 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓)) |
27 | 26 | equcoms 1695 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (𝜓 ↔ [𝑤 / 𝑦]𝜓)) |
28 | 25, 27 | bitr4id 198 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 ∈ {𝑦 ∣ 𝜓} ↔ 𝜓)) |
29 | 24, 28 | anbi12d 465 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
30 | 21, 22, 29 | cbvex 1743 |
. . . . . . . 8
⊢
(∃𝑤(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
31 | 4, 18, 30 | 3bitri 205 |
. . . . . . 7
⊢ (𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
32 | 31 | anbi2i 453 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
33 | 1, 3, 32 | 3bitr4ri 212 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
34 | 33 | exbii 1592 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
35 | | eliun 3867 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) |
36 | | df-rex 2448 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}))) |
37 | 35, 36 | bitri 183 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}))) |
38 | | elopab 4233 |
. . . 4
⊢ (𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
39 | 34, 37, 38 | 3bitr4i 211 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ↔ 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
40 | 39 | eqriv 2161 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} |
41 | | opabex3d.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
42 | | snexg 4160 |
. . . . . 6
⊢ (𝑥 ∈ V → {𝑥} ∈ V) |
43 | 11, 42 | ax-mp 5 |
. . . . 5
⊢ {𝑥} ∈ V |
44 | | opabex3d.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) |
45 | | xpexg 4715 |
. . . . 5
⊢ (({𝑥} ∈ V ∧ {𝑦 ∣ 𝜓} ∈ V) → ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
46 | 43, 44, 45 | sylancr 411 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
47 | 46 | ralrimiva 2537 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
48 | | iunexg 6082 |
. . 3
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
49 | 41, 47, 48 | syl2anc 409 |
. 2
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
50 | 40, 49 | eqeltrrid 2252 |
1
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) |