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 | | opabex3d.1 |
. . 3
⊢ (φ → A ∈
V) |
42 | | snexg 3927 |
. . . . . 6
⊢ (x ∈ V →
{x} ∈
V) |
43 | 11, 42 | ax-mp 7 |
. . . . 5
⊢ {x} ∈
V |
44 | | opabex3d.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 | ralrimiva 2386 |
. . 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 | syl2anc 391 |
. 2
⊢ (φ → ∪
x ∈
A ({x}
× {y ∣ ψ}) ∈
V) |
50 | 40, 49 | syl5eqelr 2122 |
1
⊢ (φ → {〈x, y〉
∣ (x ∈ A ∧ ψ)} ∈ V) |