Step | Hyp | Ref
| Expression |
1 | | elex 2867 |
. 2
⊢ (A ∈ V → A ∈ V) |
2 | | elex 2867 |
. 2
⊢ (B ∈ W → B ∈ V) |
3 | | elex 2867 |
. 2
⊢ (C ∈ X → C ∈ V) |
4 | | opexg 4587 |
. . . . 5
⊢ ((A ∈ V ∧ B ∈ V) → 〈A, B〉 ∈ V) |
5 | | opexg 4587 |
. . . . 5
⊢ ((〈A, B〉 ∈ V ∧ C ∈ V) →
〈〈A, B〉, C〉 ∈
V) |
6 | 4, 5 | sylan 457 |
. . . 4
⊢ (((A ∈ V ∧ B ∈ V) ∧ C ∈ V) →
〈〈A, B〉, C〉 ∈
V) |
7 | 6 | 3impa 1146 |
. . 3
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) →
〈〈A, B〉, C〉 ∈
V) |
8 | | eqeq1 2359 |
. . . . . . . . . . 11
⊢ (w = 〈〈A, B〉, C〉 →
(w = 〈〈x, y〉, z〉 ↔ 〈〈A, B〉, C〉 = 〈〈x, y〉, z〉)) |
9 | | eqcom 2355 |
. . . . . . . . . . . 12
⊢ (〈〈A, B〉, C〉 = 〈〈x, y〉, z〉 ↔ 〈〈x, y〉, z〉 = 〈〈A, B〉, C〉) |
10 | | opth 4602 |
. . . . . . . . . . . . . 14
⊢ (〈x, y〉 = 〈A, B〉 ↔
(x = A
∧ y =
B)) |
11 | 10 | anbi1i 676 |
. . . . . . . . . . . . 13
⊢ ((〈x, y〉 = 〈A, B〉 ∧ z = C) ↔ ((x =
A ∧
y = B)
∧ z =
C)) |
12 | | opth 4602 |
. . . . . . . . . . . . 13
⊢ (〈〈x, y〉, z〉 = 〈〈A, B〉, C〉 ↔ (〈x, y〉 = 〈A, B〉 ∧ z = C)) |
13 | | df-3an 936 |
. . . . . . . . . . . . 13
⊢ ((x = A ∧ y = B ∧ z = C) ↔
((x = A
∧ y =
B) ∧
z = C)) |
14 | 11, 12, 13 | 3bitr4i 268 |
. . . . . . . . . . . 12
⊢ (〈〈x, y〉, z〉 = 〈〈A, B〉, C〉 ↔
(x = A
∧ y =
B ∧
z = C)) |
15 | 9, 14 | bitri 240 |
. . . . . . . . . . 11
⊢ (〈〈A, B〉, C〉 = 〈〈x, y〉, z〉 ↔
(x = A
∧ y =
B ∧
z = C)) |
16 | 8, 15 | syl6bb 252 |
. . . . . . . . . 10
⊢ (w = 〈〈A, B〉, C〉 →
(w = 〈〈x, y〉, z〉 ↔ (x =
A ∧
y = B
∧ z =
C))) |
17 | 16 | anbi1d 685 |
. . . . . . . . 9
⊢ (w = 〈〈A, B〉, C〉 →
((w = 〈〈x, y〉, z〉 ∧ φ) ↔ ((x = A ∧ y = B ∧ z = C) ∧ φ))) |
18 | | eloprabga.1 |
. . . . . . . . . 10
⊢ ((x = A ∧ y = B ∧ z = C) →
(φ ↔ ψ)) |
19 | 18 | pm5.32i 618 |
. . . . . . . . 9
⊢ (((x = A ∧ y = B ∧ z = C) ∧ φ) ↔
((x = A
∧ y =
B ∧
z = C)
∧ ψ)) |
20 | 17, 19 | syl6bb 252 |
. . . . . . . 8
⊢ (w = 〈〈A, B〉, C〉 →
((w = 〈〈x, y〉, z〉 ∧ φ) ↔ ((x = A ∧ y = B ∧ z = C) ∧ ψ))) |
21 | 20 | 3exbidv 1629 |
. . . . . . 7
⊢ (w = 〈〈A, B〉, C〉 → (∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ) ↔
∃x∃y∃z((x = A ∧ y = B ∧ z = C) ∧ ψ))) |
22 | 21 | adantl 452 |
. . . . . 6
⊢ (((A ∈ V ∧ B ∈ V ∧ C ∈ V) ∧ w = 〈〈A, B〉, C〉) → (∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ) ↔
∃x∃y∃z((x = A ∧ y = B ∧ z = C) ∧ ψ))) |
23 | | df-oprab 5528 |
. . . . . . . . . 10
⊢ {〈〈x, y〉, z〉 ∣ φ} = {w
∣ ∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ)} |
24 | 23 | eleq2i 2417 |
. . . . . . . . 9
⊢ (w ∈ {〈〈x, y〉, z〉 ∣ φ} ↔ w ∈ {w ∣ ∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ)}) |
25 | | abid 2341 |
. . . . . . . . 9
⊢ (w ∈ {w ∣ ∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ)} ↔
∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ)) |
26 | 24, 25 | bitr2i 241 |
. . . . . . . 8
⊢ (∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ) ↔
w ∈
{〈〈x, y〉, z〉 ∣ φ}) |
27 | | eleq1 2413 |
. . . . . . . 8
⊢ (w = 〈〈A, B〉, C〉 →
(w ∈
{〈〈x, y〉, z〉 ∣ φ} ↔ 〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ})) |
28 | 26, 27 | syl5bb 248 |
. . . . . . 7
⊢ (w = 〈〈A, B〉, C〉 → (∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ) ↔
〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ})) |
29 | 28 | adantl 452 |
. . . . . 6
⊢ (((A ∈ V ∧ B ∈ V ∧ C ∈ V) ∧ w = 〈〈A, B〉, C〉) → (∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ) ↔
〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ})) |
30 | | isset 2863 |
. . . . . . . . . . . 12
⊢ (A ∈ V ↔ ∃x x = A) |
31 | | isset 2863 |
. . . . . . . . . . . 12
⊢ (B ∈ V ↔ ∃y y = B) |
32 | | isset 2863 |
. . . . . . . . . . . 12
⊢ (C ∈ V ↔ ∃z z = C) |
33 | 30, 31, 32 | 3anbi123i 1140 |
. . . . . . . . . . 11
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) ↔
(∃x
x = A
∧ ∃y y = B ∧ ∃z z = C)) |
34 | | eeeanv 1914 |
. . . . . . . . . . 11
⊢ (∃x∃y∃z(x = A ∧ y = B ∧ z = C) ↔
(∃x
x = A
∧ ∃y y = B ∧ ∃z z = C)) |
35 | 33, 34 | bitr4i 243 |
. . . . . . . . . 10
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) ↔
∃x∃y∃z(x = A ∧ y = B ∧ z = C)) |
36 | 35 | biimpi 186 |
. . . . . . . . 9
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) →
∃x∃y∃z(x = A ∧ y = B ∧ z = C)) |
37 | 36 | biantrurd 494 |
. . . . . . . 8
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) →
(ψ ↔ (∃x∃y∃z(x = A ∧ y = B ∧ z = C) ∧ ψ))) |
38 | | 19.41vvv 1903 |
. . . . . . . 8
⊢ (∃x∃y∃z((x = A ∧ y = B ∧ z = C) ∧ ψ) ↔
(∃x∃y∃z(x = A ∧ y = B ∧ z = C) ∧ ψ)) |
39 | 37, 38 | syl6rbbr 255 |
. . . . . . 7
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) →
(∃x∃y∃z((x = A ∧ y = B ∧ z = C) ∧ ψ) ↔
ψ)) |
40 | 39 | adantr 451 |
. . . . . 6
⊢ (((A ∈ V ∧ B ∈ V ∧ C ∈ V) ∧ w = 〈〈A, B〉, C〉) → (∃x∃y∃z((x = A ∧ y = B ∧ z = C) ∧ ψ) ↔
ψ)) |
41 | 22, 29, 40 | 3bitr3d 274 |
. . . . 5
⊢ (((A ∈ V ∧ B ∈ V ∧ C ∈ V) ∧ w = 〈〈A, B〉, C〉) → (〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ}
↔ ψ)) |
42 | 41 | expcom 424 |
. . . 4
⊢ (w = 〈〈A, B〉, C〉 →
((A ∈ V
∧ B ∈ V ∧ C ∈ V) →
(〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ} ↔ ψ))) |
43 | 42 | vtocleg 2925 |
. . 3
⊢ (〈〈A, B〉, C〉 ∈ V →
((A ∈ V
∧ B ∈ V ∧ C ∈ V) →
(〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ} ↔ ψ))) |
44 | 7, 43 | mpcom 32 |
. 2
⊢ ((A ∈ V ∧ B ∈ V ∧ C ∈ V) →
(〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ} ↔ ψ)) |
45 | 1, 2, 3, 44 | syl3an 1224 |
1
⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ}
↔ ψ)) |