Step | Hyp | Ref
| Expression |
1 | | 19.42v 1949 |
. . . . . 6
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) |
2 | | an12 643 |
. . . . . . 7
⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) |
3 | 2 | exbii 1842 |
. . . . . 6
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) |
4 | | elxp 5705 |
. . . . . . . 8
⊢ (𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑}) ↔ ∃𝑣∃𝑤(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
5 | | excom 2151 |
. . . . . . . . 9
⊢
(∃𝑣∃𝑤(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ ∃𝑤∃𝑣(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
6 | | an12 643 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ (𝑣 ∈ {𝑥} ∧ (𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
7 | | velsn 4648 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ {𝑥} ↔ 𝑣 = 𝑥) |
8 | 7 | anbi1i 622 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ {𝑥} ∧ (𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ (𝑣 = 𝑥 ∧ (𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
9 | 6, 8 | bitri 274 |
. . . . . . . . . . . 12
⊢ ((𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ (𝑣 = 𝑥 ∧ (𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
10 | 9 | exbii 1842 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ ∃𝑣(𝑣 = 𝑥 ∧ (𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
11 | | opeq1 4878 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑥 → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑤⟩) |
12 | 11 | eqeq2d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑥 → (𝑧 = ⟨𝑣, 𝑤⟩ ↔ 𝑧 = ⟨𝑥, 𝑤⟩)) |
13 | 12 | anbi1d 629 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑥 → ((𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}) ↔ (𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}))) |
14 | 13 | equsexvw 2000 |
. . . . . . . . . . 11
⊢
(∃𝑣(𝑣 = 𝑥 ∧ (𝑧 = ⟨𝑣, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ (𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) |
15 | 10, 14 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑣(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ (𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) |
16 | 15 | exbii 1842 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ ∃𝑤(𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) |
17 | 5, 16 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑣∃𝑤(𝑧 = ⟨𝑣, 𝑤⟩ ∧ (𝑣 ∈ {𝑥} ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) ↔ ∃𝑤(𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑})) |
18 | | nfv 1909 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑧 = ⟨𝑥, 𝑤⟩ |
19 | | nfsab1 2713 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑤 ∈ {𝑦 ∣ 𝜑} |
20 | 18, 19 | nfan 1894 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}) |
21 | | nfv 1909 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) |
22 | | opeq2 4879 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → ⟨𝑥, 𝑤⟩ = ⟨𝑥, 𝑦⟩) |
23 | 22 | eqeq2d 2739 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑧 = ⟨𝑥, 𝑤⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩)) |
24 | | df-clab 2706 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑦 ∣ 𝜑} ↔ [𝑤 / 𝑦]𝜑) |
25 | | sbequ12 2238 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑦]𝜑)) |
26 | 25 | equcoms 2015 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (𝜑 ↔ [𝑤 / 𝑦]𝜑)) |
27 | 24, 26 | bitr4id 289 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 ∈ {𝑦 ∣ 𝜑} ↔ 𝜑)) |
28 | 23, 27 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) |
29 | 20, 21, 28 | cbvexv1 2333 |
. . . . . . . 8
⊢
(∃𝑤(𝑧 = ⟨𝑥, 𝑤⟩ ∧ 𝑤 ∈ {𝑦 ∣ 𝜑}) ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) |
30 | 4, 17, 29 | 3bitri 296 |
. . . . . . 7
⊢ (𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑}) ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) |
31 | 30 | anbi2i 621 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑})) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) |
32 | 1, 3, 31 | 3bitr4ri 303 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑})) ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
33 | 32 | exbii 1842 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑})) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
34 | | eliun 5004 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑})) |
35 | | df-rex 3068 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑}) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑}))) |
36 | 34, 35 | bitri 274 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑥} × {𝑦 ∣ 𝜑}))) |
37 | | elopab 5533 |
. . . 4
⊢ (𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
38 | 33, 36, 37 | 3bitr4i 302 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ↔ 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
39 | 38 | eqriv 2725 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
40 | | opabex3.1 |
. . 3
⊢ 𝐴 ∈ V |
41 | | vsnex 5435 |
. . . . 5
⊢ {𝑥} ∈ V |
42 | | opabex3.2 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) |
43 | | xpexg 7758 |
. . . . 5
⊢ (({𝑥} ∈ V ∧ {𝑦 ∣ 𝜑} ∈ V) → ({𝑥} × {𝑦 ∣ 𝜑}) ∈ V) |
44 | 41, 42, 43 | sylancr 585 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ({𝑥} × {𝑦 ∣ 𝜑}) ∈ V) |
45 | 44 | rgen 3060 |
. . 3
⊢
∀𝑥 ∈
𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ∈ V |
46 | | iunexg 7973 |
. . 3
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ∈ V) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ∈ V) |
47 | 40, 45, 46 | mp2an 690 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝑦 ∣ 𝜑}) ∈ V |
48 | 39, 47 | eqeltrri 2826 |
1
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V |