Step | Hyp | Ref
| Expression |
1 | | 19.42v 1783 |
. . . . . 6
⊢ (∃y(x ∈ A ∧ (z = 〈x,
y〉 ∧
φ)) ↔ (x ∈ A ∧ ∃y(z = 〈x,
y〉 ∧
φ))) |
2 | | an12 495 |
. . . . . . 7
⊢
((z = 〈x, y〉 ∧ (x ∈ A ∧ φ)) ↔
(x ∈
A ∧
(z = 〈x, y〉 ∧ φ))) |
3 | 2 | exbii 1493 |
. . . . . 6
⊢ (∃y(z = 〈x,
y〉 ∧
(x ∈
A ∧ φ)) ↔ ∃y(x ∈ A ∧ (z = 〈x,
y〉 ∧
φ))) |
4 | | elxp 4305 |
. . . . . . . 8
⊢ (z ∈ ({x} × {y
∣ φ}) ↔ ∃v∃w(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ}))) |
5 | | excom 1551 |
. . . . . . . . 9
⊢ (∃v∃w(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ})) ↔ ∃w∃v(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ}))) |
6 | | an12 495 |
. . . . . . . . . . . . 13
⊢
((z = 〈v, w〉 ∧ (v ∈ {x} ∧ w ∈ {y ∣
φ})) ↔ (v ∈ {x} ∧ (z = 〈v,
w〉 ∧
w ∈
{y ∣ φ}))) |
7 | | elsn 3382 |
. . . . . . . . . . . . . 14
⊢ (v ∈ {x} ↔ v =
x) |
8 | 7 | anbi1i 431 |
. . . . . . . . . . . . 13
⊢
((v ∈ {x} ∧ (z =
〈v, w〉 ∧ w ∈ {y ∣ φ})) ↔ (v = x ∧ (z =
〈v, w〉 ∧ w ∈ {y ∣ φ}))) |
9 | 6, 8 | bitri 173 |
. . . . . . . . . . . 12
⊢
((z = 〈v, w〉 ∧ (v ∈ {x} ∧ w ∈ {y ∣
φ})) ↔ (v = x ∧ (z =
〈v, w〉 ∧ w ∈ {y ∣ φ}))) |
10 | 9 | exbii 1493 |
. . . . . . . . . . 11
⊢ (∃v(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ})) ↔ ∃v(v = x ∧ (z =
〈v, w〉 ∧ w ∈ {y ∣ φ}))) |
11 | | vex 2554 |
. . . . . . . . . . . 12
⊢ x ∈
V |
12 | | opeq1 3540 |
. . . . . . . . . . . . . 14
⊢ (v = x →
〈v, w〉 = 〈x, w〉) |
13 | 12 | eqeq2d 2048 |
. . . . . . . . . . . . 13
⊢ (v = x →
(z = 〈v, w〉
↔ z = 〈x, w〉)) |
14 | 13 | anbi1d 438 |
. . . . . . . . . . . 12
⊢ (v = x →
((z = 〈v, w〉 ∧ w ∈ {y ∣
φ}) ↔ (z = 〈x,
w〉 ∧
w ∈
{y ∣ φ}))) |
15 | 11, 14 | ceqsexv 2587 |
. . . . . . . . . . 11
⊢ (∃v(v = x ∧ (z =
〈v, w〉 ∧ w ∈ {y ∣ φ})) ↔ (z = 〈x,
w〉 ∧
w ∈
{y ∣ φ})) |
16 | 10, 15 | bitri 173 |
. . . . . . . . . 10
⊢ (∃v(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ})) ↔ (z = 〈x,
w〉 ∧
w ∈
{y ∣ φ})) |
17 | 16 | exbii 1493 |
. . . . . . . . 9
⊢ (∃w∃v(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ})) ↔ ∃w(z = 〈x,
w〉 ∧
w ∈
{y ∣ φ})) |
18 | 5, 17 | bitri 173 |
. . . . . . . 8
⊢ (∃v∃w(z = 〈v,
w〉 ∧
(v ∈
{x} ∧
w ∈
{y ∣ φ})) ↔ ∃w(z = 〈x,
w〉 ∧
w ∈
{y ∣ φ})) |
19 | | nfv 1418 |
. . . . . . . . . 10
⊢
Ⅎy z = 〈x,
w〉 |
20 | | nfsab1 2027 |
. . . . . . . . . 10
⊢
Ⅎy w ∈ {y ∣ φ} |
21 | 19, 20 | nfan 1454 |
. . . . . . . . 9
⊢
Ⅎy(z = 〈x,
w〉 ∧
w ∈
{y ∣ φ}) |
22 | | nfv 1418 |
. . . . . . . . 9
⊢
Ⅎw(z = 〈x,
y〉 ∧
φ) |
23 | | opeq2 3541 |
. . . . . . . . . . 11
⊢ (w = y →
〈x, w〉 = 〈x, y〉) |
24 | 23 | eqeq2d 2048 |
. . . . . . . . . 10
⊢ (w = y →
(z = 〈x, w〉
↔ z = 〈x, y〉)) |
25 | | sbequ12 1651 |
. . . . . . . . . . . 12
⊢ (y = w →
(φ ↔ [w / y]φ)) |
26 | 25 | equcoms 1591 |
. . . . . . . . . . 11
⊢ (w = y →
(φ ↔ [w / y]φ)) |
27 | | df-clab 2024 |
. . . . . . . . . . 11
⊢ (w ∈ {y ∣ φ}
↔ [w / y]φ) |
28 | 26, 27 | syl6rbbr 188 |
. . . . . . . . . 10
⊢ (w = y →
(w ∈
{y ∣ φ} ↔ φ)) |
29 | 24, 28 | anbi12d 442 |
. . . . . . . . 9
⊢ (w = y →
((z = 〈x, w〉 ∧ w ∈ {y ∣
φ}) ↔ (z = 〈x,
y〉 ∧
φ))) |
30 | 21, 22, 29 | cbvex 1636 |
. . . . . . . 8
⊢ (∃w(z = 〈x,
w〉 ∧
w ∈
{y ∣ φ}) ↔ ∃y(z = 〈x,
y〉 ∧
φ)) |
31 | 4, 18, 30 | 3bitri 195 |
. . . . . . 7
⊢ (z ∈ ({x} × {y
∣ φ}) ↔ ∃y(z = 〈x,
y〉 ∧
φ)) |
32 | 31 | anbi2i 430 |
. . . . . 6
⊢
((x ∈ A ∧ z ∈ ({x} ×
{y ∣ φ})) ↔ (x ∈ A ∧ ∃y(z = 〈x,
y〉 ∧
φ))) |
33 | 1, 3, 32 | 3bitr4ri 202 |
. . . . 5
⊢
((x ∈ A ∧ z ∈ ({x} ×
{y ∣ φ})) ↔ ∃y(z = 〈x,
y〉 ∧
(x ∈
A ∧ φ))) |
34 | 33 | exbii 1493 |
. . . 4
⊢ (∃x(x ∈ A ∧ z ∈ ({x} × {y
∣ φ})) ↔ ∃x∃y(z = 〈x,
y〉 ∧
(x ∈
A ∧ φ))) |
35 | | eliun 3652 |
. . . . 5
⊢ (z ∈ ∪ x ∈ A ({x} × {y
∣ φ}) ↔ ∃x ∈ A z ∈ ({x} × {y
∣ φ})) |
36 | | df-rex 2306 |
. . . . 5
⊢ (∃x ∈ A z ∈ ({x} × {y
∣ φ}) ↔ ∃x(x ∈ A ∧ z ∈ ({x} × {y
∣ φ}))) |
37 | 35, 36 | bitri 173 |
. . . 4
⊢ (z ∈ ∪ x ∈ A ({x} × {y
∣ φ}) ↔ ∃x(x ∈ A ∧ z ∈ ({x} × {y
∣ φ}))) |
38 | | elopab 3986 |
. . . 4
⊢ (z ∈
{〈x, y〉 ∣ (x ∈ A ∧ φ)} ↔ ∃x∃y(z = 〈x,
y〉 ∧
(x ∈
A ∧ φ))) |
39 | 34, 37, 38 | 3bitr4i 201 |
. . 3
⊢ (z ∈ ∪ x ∈ A ({x} × {y
∣ φ}) ↔ z ∈
{〈x, y〉 ∣ (x ∈ A ∧ φ)}) |
40 | 39 | eqriv 2034 |
. 2
⊢ ∪ x ∈ A ({x} × {y
∣ φ}) = {〈x, y〉
∣ (x ∈ A ∧ φ)} |
41 | | opabex3.1 |
. . 3
⊢ A ∈
V |
42 | | snexg 3927 |
. . . . . 6
⊢ (x ∈ V →
{x} ∈
V) |
43 | 11, 42 | ax-mp 7 |
. . . . 5
⊢ {x} ∈
V |
44 | | opabex3.2 |
. . . . 5
⊢ (x ∈ A → {y
∣ φ} ∈ V) |
45 | | xpexg 4395 |
. . . . 5
⊢
(({x} ∈ V ∧ {y ∣ φ}
∈ V) → ({x} × {y
∣ φ}) ∈ V) |
46 | 43, 44, 45 | sylancr 393 |
. . . 4
⊢ (x ∈ A → ({x}
× {y ∣ φ}) ∈
V) |
47 | 46 | rgen 2368 |
. . 3
⊢ ∀x ∈ A ({x} × {y
∣ φ}) ∈ V |
48 | | iunexg 5688 |
. . 3
⊢
((A ∈ V ∧ ∀x ∈ A ({x} × {y
∣ φ}) ∈ V) → ∪
x ∈
A ({x}
× {y ∣ φ}) ∈
V) |
49 | 41, 47, 48 | mp2an 402 |
. 2
⊢ ∪ x ∈ A ({x} × {y
∣ φ}) ∈ V |
50 | 40, 49 | eqeltrri 2108 |
1
⊢
{〈x, y〉 ∣ (x ∈ A ∧ φ)} ∈
V |