Step | Hyp | Ref
| Expression |
1 | | elex 2560 |
. 2
⊢
(〈x, 𝐶〉 ∈
∪ x ∈ A ({x} × B)
→ 〈x, 𝐶〉 ∈
V) |
2 | | vex 2554 |
. . 3
⊢ x ∈
V |
3 | | elex 2560 |
. . . 4
⊢ (𝐶 ∈ B →
𝐶 ∈ V) |
4 | 3 | adantl 262 |
. . 3
⊢
((x ∈ A ∧ 𝐶 ∈
B) → 𝐶 ∈
V) |
5 | | opexgOLD 3956 |
. . 3
⊢
((x ∈ V ∧ 𝐶 ∈ V) → 〈x, 𝐶〉 ∈
V) |
6 | 2, 4, 5 | sylancr 393 |
. 2
⊢
((x ∈ A ∧ 𝐶 ∈
B) → 〈x, 𝐶〉 ∈
V) |
7 | | df-rex 2306 |
. . . . . 6
⊢ (∃x ∈ A y ∈ ({x} × B)
↔ ∃x(x ∈ A ∧ y ∈ ({x} ×
B))) |
8 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎz(x ∈ A ∧ y ∈ ({x} × B)) |
9 | | nfs1v 1812 |
. . . . . . . 8
⊢
Ⅎx[z / x]x ∈ A |
10 | | nfcv 2175 |
. . . . . . . . . 10
⊢
Ⅎx{z} |
11 | | nfcsb1v 2876 |
. . . . . . . . . 10
⊢
Ⅎx⦋z / x⦌B |
12 | 10, 11 | nfxp 4314 |
. . . . . . . . 9
⊢
Ⅎx({z} × ⦋z / x⦌B) |
13 | 12 | nfcri 2169 |
. . . . . . . 8
⊢
Ⅎx y ∈ ({z} × ⦋z / x⦌B) |
14 | 9, 13 | nfan 1454 |
. . . . . . 7
⊢
Ⅎx([z / x]x ∈ A ∧ y ∈ ({z} × ⦋z / x⦌B)) |
15 | | sbequ12 1651 |
. . . . . . . 8
⊢ (x = z →
(x ∈
A ↔ [z / x]x ∈ A)) |
16 | | sneq 3378 |
. . . . . . . . . 10
⊢ (x = z →
{x} = {z}) |
17 | | csbeq1a 2854 |
. . . . . . . . . 10
⊢ (x = z →
B = ⦋z / x⦌B) |
18 | 16, 17 | xpeq12d 4313 |
. . . . . . . . 9
⊢ (x = z →
({x} × B) = ({z}
× ⦋z / x⦌B)) |
19 | 18 | eleq2d 2104 |
. . . . . . . 8
⊢ (x = z →
(y ∈
({x} × B) ↔ y
∈ ({z}
× ⦋z / x⦌B))) |
20 | 15, 19 | anbi12d 442 |
. . . . . . 7
⊢ (x = z →
((x ∈
A ∧
y ∈
({x} × B)) ↔ ([z /
x]x
∈ A ∧ y ∈ ({z} ×
⦋z / x⦌B)))) |
21 | 8, 14, 20 | cbvex 1636 |
. . . . . 6
⊢ (∃x(x ∈ A ∧ y ∈ ({x} × B))
↔ ∃z([z / x]x ∈ A ∧ y ∈ ({z} ×
⦋z / x⦌B))) |
22 | 7, 21 | bitri 173 |
. . . . 5
⊢ (∃x ∈ A y ∈ ({x} × B)
↔ ∃z([z / x]x ∈ A ∧ y ∈ ({z} ×
⦋z / x⦌B))) |
23 | | eleq1 2097 |
. . . . . . 7
⊢ (y = 〈x,
𝐶〉 → (y ∈ ({z} × ⦋z / x⦌B) ↔ 〈x, 𝐶〉 ∈
({z} × ⦋z / x⦌B))) |
24 | 23 | anbi2d 437 |
. . . . . 6
⊢ (y = 〈x,
𝐶〉 → (([z / x]x ∈ A ∧ y ∈ ({z} × ⦋z / x⦌B)) ↔ ([z /
x]x
∈ A ∧ 〈x, 𝐶〉 ∈ ({z} ×
⦋z / x⦌B)))) |
25 | 24 | exbidv 1703 |
. . . . 5
⊢ (y = 〈x,
𝐶〉 → (∃z([z / x]x ∈ A ∧ y ∈ ({z} × ⦋z / x⦌B)) ↔ ∃z([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈
({z} × ⦋z / x⦌B)))) |
26 | 22, 25 | syl5bb 181 |
. . . 4
⊢ (y = 〈x,
𝐶〉 → (∃x ∈ A y ∈ ({x} × B)
↔ ∃z([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈ ({z} ×
⦋z / x⦌B)))) |
27 | | df-iun 3650 |
. . . 4
⊢ ∪ x ∈ A ({x} × B) =
{y ∣ ∃x ∈ A y ∈ ({x} × B)} |
28 | 26, 27 | elab2g 2683 |
. . 3
⊢
(〈x, 𝐶〉 ∈ V
→ (〈x, 𝐶〉 ∈
∪ x ∈ A ({x} × B)
↔ ∃z([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈ ({z} ×
⦋z / x⦌B)))) |
29 | | opelxp 4317 |
. . . . . . 7
⊢
(〈x, 𝐶〉 ∈
({z} × ⦋z / x⦌B) ↔ (x
∈ {z}
∧ 𝐶 ∈
⦋z / x⦌B)) |
30 | 29 | anbi2i 430 |
. . . . . 6
⊢
(([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈ ({z} ×
⦋z / x⦌B)) ↔ ([z /
x]x
∈ A ∧ (x ∈ {z} ∧ 𝐶 ∈
⦋z / x⦌B))) |
31 | | an12 495 |
. . . . . 6
⊢
(([z / x]x ∈ A ∧ (x ∈ {z} ∧ 𝐶 ∈
⦋z / x⦌B)) ↔ (x
∈ {z}
∧ ([z /
x]x
∈ A ∧ 𝐶 ∈
⦋z / x⦌B))) |
32 | | elsn 3382 |
. . . . . . . 8
⊢ (x ∈ {z} ↔ x =
z) |
33 | | equcom 1590 |
. . . . . . . 8
⊢ (x = z ↔
z = x) |
34 | 32, 33 | bitri 173 |
. . . . . . 7
⊢ (x ∈ {z} ↔ z =
x) |
35 | 34 | anbi1i 431 |
. . . . . 6
⊢
((x ∈ {z} ∧ ([z / x]x ∈ A ∧ 𝐶 ∈
⦋z / x⦌B)) ↔ (z =
x ∧
([z / x]x ∈ A ∧ 𝐶 ∈
⦋z / x⦌B))) |
36 | 30, 31, 35 | 3bitri 195 |
. . . . 5
⊢
(([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈ ({z} ×
⦋z / x⦌B)) ↔ (z =
x ∧
([z / x]x ∈ A ∧ 𝐶 ∈
⦋z / x⦌B))) |
37 | 36 | exbii 1493 |
. . . 4
⊢ (∃z([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈
({z} × ⦋z / x⦌B)) ↔ ∃z(z = x ∧ ([z / x]x ∈ A ∧ 𝐶 ∈
⦋z / x⦌B))) |
38 | | sbequ12r 1652 |
. . . . . 6
⊢ (z = x →
([z / x]x ∈ A ↔
x ∈
A)) |
39 | 17 | equcoms 1591 |
. . . . . . . 8
⊢ (z = x →
B = ⦋z / x⦌B) |
40 | 39 | eqcomd 2042 |
. . . . . . 7
⊢ (z = x →
⦋z / x⦌B = B) |
41 | 40 | eleq2d 2104 |
. . . . . 6
⊢ (z = x →
(𝐶 ∈ ⦋z / x⦌B ↔ 𝐶 ∈
B)) |
42 | 38, 41 | anbi12d 442 |
. . . . 5
⊢ (z = x →
(([z / x]x ∈ A ∧ 𝐶 ∈
⦋z / x⦌B) ↔ (x
∈ A ∧ 𝐶 ∈
B))) |
43 | 2, 42 | ceqsexv 2587 |
. . . 4
⊢ (∃z(z = x ∧ ([z / x]x ∈ A ∧ 𝐶 ∈
⦋z / x⦌B)) ↔ (x
∈ A ∧ 𝐶 ∈
B)) |
44 | 37, 43 | bitri 173 |
. . 3
⊢ (∃z([z / x]x ∈ A ∧ 〈x, 𝐶〉 ∈
({z} × ⦋z / x⦌B)) ↔ (x
∈ A ∧ 𝐶 ∈
B)) |
45 | 28, 44 | syl6bb 185 |
. 2
⊢
(〈x, 𝐶〉 ∈ V
→ (〈x, 𝐶〉 ∈
∪ x ∈ A ({x} × B)
↔ (x ∈ A ∧ 𝐶 ∈
B))) |
46 | 1, 6, 45 | pm5.21nii 619 |
1
⊢
(〈x, 𝐶〉 ∈
∪ x ∈ A ({x} × B)
↔ (x ∈ A ∧ 𝐶 ∈
B)) |