Step | Hyp | Ref
| Expression |
1 | | euotd.1 |
. . . 4
⊢ (φ → A ∈
V) |
2 | | euotd.2 |
. . . 4
⊢ (φ → B ∈
V) |
3 | | euotd.3 |
. . . 4
⊢ (φ → 𝐶 ∈
V) |
4 | | otexg 3958 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V ∧ 𝐶 ∈ V)
→ 〈A, B, 𝐶〉 ∈
V) |
5 | 1, 2, 3, 4 | syl3anc 1134 |
. . 3
⊢ (φ → 〈A, B, 𝐶〉 ∈ V) |
6 | | euotd.4 |
. . . . . . . . . . . . 13
⊢ (φ → (ψ ↔ (𝑎 = A
∧ 𝑏 = B
∧ 𝑐 = 𝐶))) |
7 | 6 | biimpa 280 |
. . . . . . . . . . . 12
⊢ ((φ ∧ ψ) → (𝑎 = A
∧ 𝑏 = B
∧ 𝑐 = 𝐶)) |
8 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
9 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ V |
10 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ 𝑐 ∈ V |
11 | 8, 9, 10 | otth 3970 |
. . . . . . . . . . . 12
⊢
(〈𝑎, 𝑏, 𝑐〉 = 〈A, B, 𝐶〉 ↔ (𝑎 = A
∧ 𝑏 = B
∧ 𝑐 = 𝐶)) |
12 | 7, 11 | sylibr 137 |
. . . . . . . . . . 11
⊢ ((φ ∧ ψ) → 〈𝑎, 𝑏, 𝑐〉 = 〈A, B, 𝐶〉) |
13 | 12 | eqeq2d 2048 |
. . . . . . . . . 10
⊢ ((φ ∧ ψ) → (x = 〈𝑎, 𝑏, 𝑐〉 ↔ x = 〈A,
B, 𝐶〉)) |
14 | 13 | biimpd 132 |
. . . . . . . . 9
⊢ ((φ ∧ ψ) → (x = 〈𝑎, 𝑏, 𝑐〉 → x = 〈A,
B, 𝐶〉)) |
15 | 14 | impancom 247 |
. . . . . . . 8
⊢ ((φ ∧ x = 〈𝑎, 𝑏, 𝑐〉) → (ψ → x = 〈A,
B, 𝐶〉)) |
16 | 15 | expimpd 345 |
. . . . . . 7
⊢ (φ → ((x = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) → x = 〈A,
B, 𝐶〉)) |
17 | 16 | exlimdv 1697 |
. . . . . 6
⊢ (φ → (∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) → x = 〈A,
B, 𝐶〉)) |
18 | 17 | exlimdvv 1774 |
. . . . 5
⊢ (φ → (∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) → x = 〈A,
B, 𝐶〉)) |
19 | | tru 1246 |
. . . . . . . . . . 11
⊢
⊤ |
20 | 2 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ 𝑎 = A) → B
∈ V) |
21 | 3 | ad2antrr 457 |
. . . . . . . . . . . . . 14
⊢ (((φ ∧ 𝑎 = A) ∧ 𝑏 = B) → 𝐶 ∈
V) |
22 | | simpr 103 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → (𝑎 = A
∧ 𝑏 = B
∧ 𝑐 = 𝐶)) |
23 | 22, 11 | sylibr 137 |
. . . . . . . . . . . . . . . . . 18
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → 〈𝑎, 𝑏, 𝑐〉 = 〈A, B, 𝐶〉) |
24 | 23 | eqcomd 2042 |
. . . . . . . . . . . . . . . . 17
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → 〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉) |
25 | 6 | biimpar 281 |
. . . . . . . . . . . . . . . . 17
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → ψ) |
26 | 24, 25 | jca 290 |
. . . . . . . . . . . . . . . 16
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → (〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
27 | | a1tru 1258 |
. . . . . . . . . . . . . . . 16
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → ⊤ ) |
28 | 26, 27 | 2thd 164 |
. . . . . . . . . . . . . . 15
⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B
∧ 𝑐 = 𝐶)) → ((〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ⊤ )) |
29 | 28 | 3anassrs 1125 |
. . . . . . . . . . . . . 14
⊢ ((((φ ∧ 𝑎 = A) ∧ 𝑏 = B) ∧ 𝑐 = 𝐶) → ((〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ⊤ )) |
30 | 21, 29 | sbcied 2793 |
. . . . . . . . . . . . 13
⊢ (((φ ∧ 𝑎 = A) ∧ 𝑏 = B) → ([𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ⊤ )) |
31 | 20, 30 | sbcied 2793 |
. . . . . . . . . . . 12
⊢ ((φ ∧ 𝑎 = A) → ([B / 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ⊤ )) |
32 | 1, 31 | sbcied 2793 |
. . . . . . . . . . 11
⊢ (φ → ([A / 𝑎][B / 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ⊤ )) |
33 | 19, 32 | mpbiri 157 |
. . . . . . . . . 10
⊢ (φ → [A / 𝑎][B / 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
34 | 33 | spesbcd 2838 |
. . . . . . . . 9
⊢ (φ → ∃𝑎[B
/ 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
35 | | nfcv 2175 |
. . . . . . . . . 10
⊢
Ⅎ𝑏B |
36 | | nfsbc1v 2776 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏[B
/ 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) |
37 | 36 | nfex 1525 |
. . . . . . . . . 10
⊢
Ⅎ𝑏∃𝑎[B
/ 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) |
38 | | sbceq1a 2767 |
. . . . . . . . . . 11
⊢ (𝑏 = B → ([𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ [B / 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
39 | 38 | exbidv 1703 |
. . . . . . . . . 10
⊢ (𝑏 = B → (∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ∃𝑎[B
/ 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
40 | 35, 37, 39 | spcegf 2630 |
. . . . . . . . 9
⊢ (B ∈ V →
(∃𝑎[B
/ 𝑏][𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) → ∃𝑏∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
41 | 2, 34, 40 | sylc 56 |
. . . . . . . 8
⊢ (φ → ∃𝑏∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
42 | | nfcv 2175 |
. . . . . . . . 9
⊢
Ⅎ𝑐𝐶 |
43 | | nfsbc1v 2776 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) |
44 | 43 | nfex 1525 |
. . . . . . . . . 10
⊢
Ⅎ𝑐∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) |
45 | 44 | nfex 1525 |
. . . . . . . . 9
⊢
Ⅎ𝑐∃𝑏∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) |
46 | | sbceq1a 2767 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → ((〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ [𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
47 | 46 | 2exbidv 1745 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (∃𝑏∃𝑎(〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ∃𝑏∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
48 | 42, 45, 47 | spcegf 2630 |
. . . . . . . 8
⊢ (𝐶 ∈ V → (∃𝑏∃𝑎[𝐶 / 𝑐](〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) → ∃𝑐∃𝑏∃𝑎(〈A,
B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
49 | 3, 41, 48 | sylc 56 |
. . . . . . 7
⊢ (φ → ∃𝑐∃𝑏∃𝑎(〈A,
B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
50 | | excom13 1576 |
. . . . . . 7
⊢ (∃𝑐∃𝑏∃𝑎(〈A,
B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ∃𝑎∃𝑏∃𝑐(〈A,
B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
51 | 49, 50 | sylib 127 |
. . . . . 6
⊢ (φ → ∃𝑎∃𝑏∃𝑐(〈A,
B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |
52 | | eqeq1 2043 |
. . . . . . . 8
⊢ (x = 〈A,
B, 𝐶〉 → (x = 〈𝑎, 𝑏, 𝑐〉 ↔ 〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉)) |
53 | 52 | anbi1d 438 |
. . . . . . 7
⊢ (x = 〈A,
B, 𝐶〉 → ((x = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ (〈A, B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
54 | 53 | 3exbidv 1746 |
. . . . . 6
⊢ (x = 〈A,
B, 𝐶〉 → (∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ∃𝑎∃𝑏∃𝑐(〈A,
B, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
55 | 51, 54 | syl5ibrcom 146 |
. . . . 5
⊢ (φ → (x = 〈A,
B, 𝐶〉 → ∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ))) |
56 | 18, 55 | impbid 120 |
. . . 4
⊢ (φ → (∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = 〈A,
B, 𝐶〉)) |
57 | 56 | alrimiv 1751 |
. . 3
⊢ (φ → ∀x(∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = 〈A,
B, 𝐶〉)) |
58 | | eqeq2 2046 |
. . . . . 6
⊢ (y = 〈A,
B, 𝐶〉 → (x = y ↔
x = 〈A, B, 𝐶〉)) |
59 | 58 | bibi2d 221 |
. . . . 5
⊢ (y = 〈A,
B, 𝐶〉 → ((∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = y) ↔
(∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = 〈A,
B, 𝐶〉))) |
60 | 59 | albidv 1702 |
. . . 4
⊢ (y = 〈A,
B, 𝐶〉 → (∀x(∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = y) ↔
∀x(∃𝑎∃𝑏∃𝑐(x = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = 〈A,
B, 𝐶〉))) |
61 | 60 | spcegv 2635 |
. . 3
⊢
(〈A, B, 𝐶〉 ∈ V
→ (∀x(∃𝑎∃𝑏∃𝑐(x = 〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = 〈A,
B, 𝐶〉) → ∃y∀x(∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = y))) |
62 | 5, 57, 61 | sylc 56 |
. 2
⊢ (φ → ∃y∀x(∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = y)) |
63 | | df-eu 1900 |
. 2
⊢ (∃!x∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ ∃y∀x(∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ) ↔ x = y)) |
64 | 62, 63 | sylibr 137 |
1
⊢ (φ → ∃!x∃𝑎∃𝑏∃𝑐(x =
〈𝑎, 𝑏, 𝑐〉 ∧
ψ)) |