Step | Hyp | Ref
| Expression |
1 | | 19.42v 2052 |
. . . . . 6
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
2 | | an12 635 |
. . . . . . 7
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
3 | 2 | exbii 1947 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
4 | | elxp 5369 |
. . . . . . . 8
⊢ (𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑣∃𝑤(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
5 | | excom 2212 |
. . . . . . . . 9
⊢
(∃𝑣∃𝑤(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑤∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
6 | | an12 635 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑣 ∈ {𝑥} ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
7 | | velsn 4415 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑥} ↔ 𝑣 = 𝑥) |
8 | 7 | anbi1i 617 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ {𝑥} ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
9 | 6, 8 | bitri 267 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
10 | 9 | exbii 1947 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑣(𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
11 | | vex 3417 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | opeq1 4625 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑥 → 〈𝑣, 𝑤〉 = 〈𝑥, 𝑤〉) |
13 | 12 | eqeq2d 2835 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑥 → (𝑧 = 〈𝑣, 𝑤〉 ↔ 𝑧 = 〈𝑥, 𝑤〉)) |
14 | 13 | anbi1d 623 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑥 → ((𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) ↔ (𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}))) |
15 | 11, 14 | ceqsexv 3459 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑣 = 𝑥 ∧ (𝑧 = 〈𝑣, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
16 | 10, 15 | bitri 267 |
. . . . . . . . . 10
⊢
(∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ (𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
17 | 16 | exbii 1947 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑤(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
18 | 5, 17 | bitri 267 |
. . . . . . . 8
⊢
(∃𝑣∃𝑤(𝑧 = 〈𝑣, 𝑤〉 ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) ↔ ∃𝑤(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓})) |
19 | | nfv 2013 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑧 = 〈𝑥, 𝑤〉 |
20 | | nfsab1 2815 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑤 ∈ {𝑦 ∣ 𝜓} |
21 | 19, 20 | nfan 2002 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) |
22 | | nfv 2013 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) |
23 | | opeq2 4626 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → 〈𝑥, 𝑤〉 = 〈𝑥, 𝑦〉) |
24 | 23 | eqeq2d 2835 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑧 = 〈𝑥, 𝑤〉 ↔ 𝑧 = 〈𝑥, 𝑦〉)) |
25 | | sbequ12 2286 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓)) |
26 | 25 | equcoms 2124 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (𝜓 ↔ [𝑤 / 𝑦]𝜓)) |
27 | | df-clab 2812 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑦 ∣ 𝜓} ↔ [𝑤 / 𝑦]𝜓) |
28 | 26, 27 | syl6rbbr 282 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 ∈ {𝑦 ∣ 𝜓} ↔ 𝜓)) |
29 | 24, 28 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
30 | 21, 22, 29 | cbvexv1 2368 |
. . . . . . . 8
⊢
(∃𝑤(𝑧 = 〈𝑥, 𝑤〉 ∧ 𝑤 ∈ {𝑦 ∣ 𝜓}) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
31 | 4, 18, 30 | 3bitri 289 |
. . . . . . 7
⊢ (𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)) |
32 | 31 | anbi2i 616 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓))) |
33 | 1, 3, 32 | 3bitr4ri 296 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
34 | 33 | exbii 1947 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
35 | | eliun 4746 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓})) |
36 | | df-rex 3123 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}))) |
37 | 35, 36 | bitri 267 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜓}))) |
38 | | elopab 5211 |
. . . 4
⊢ (𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
39 | 34, 37, 38 | 3bitr4i 295 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ↔ 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
40 | 39 | eqriv 2822 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} |
41 | | opabex3d.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
42 | | snex 5131 |
. . . . 5
⊢ {𝑥} ∈ V |
43 | | opabex3d.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) |
44 | | xpexg 7225 |
. . . . 5
⊢ (({𝑥} ∈ V ∧ {𝑦 ∣ 𝜓} ∈ V) → ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
45 | 42, 43, 44 | sylancr 581 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
46 | 45 | ralrimiva 3175 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
47 | | iunexg 7409 |
. . 3
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
48 | 41, 46, 47 | syl2anc 579 |
. 2
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜓}) ∈ V) |
49 | 40, 48 | syl5eqelr 2911 |
1
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) |