Step | Hyp | Ref
| Expression |
1 | | reuind.2 |
. . . . . . . 8
⊢ (x = y →
A = B) |
2 | 1 | eleq1d 2103 |
. . . . . . 7
⊢ (x = y →
(A ∈
𝐶 ↔ B ∈ 𝐶)) |
3 | | reuind.1 |
. . . . . . 7
⊢ (x = y →
(φ ↔ ψ)) |
4 | 2, 3 | anbi12d 442 |
. . . . . 6
⊢ (x = y →
((A ∈
𝐶 ∧ φ) ↔
(B ∈
𝐶 ∧ ψ))) |
5 | 4 | cbvexv 1792 |
. . . . 5
⊢ (∃x(A ∈ 𝐶 ∧ φ) ↔
∃y(B ∈ 𝐶 ∧ ψ)) |
6 | | r19.41v 2460 |
. . . . . . 7
⊢ (∃z ∈ 𝐶 (z =
B ∧ ψ) ↔ (∃z ∈ 𝐶 z =
B ∧ ψ)) |
7 | 6 | exbii 1493 |
. . . . . 6
⊢ (∃y∃z ∈ 𝐶 (z =
B ∧ ψ) ↔ ∃y(∃z ∈ 𝐶 z =
B ∧ ψ)) |
8 | | rexcom4 2571 |
. . . . . 6
⊢ (∃z ∈ 𝐶 ∃y(z = B ∧ ψ) ↔
∃y∃z ∈ 𝐶 (z =
B ∧ ψ)) |
9 | | risset 2346 |
. . . . . . . 8
⊢ (B ∈ 𝐶 ↔ ∃z ∈ 𝐶 z =
B) |
10 | 9 | anbi1i 431 |
. . . . . . 7
⊢
((B ∈ 𝐶 ∧ ψ) ↔ (∃z ∈ 𝐶 z =
B ∧ ψ)) |
11 | 10 | exbii 1493 |
. . . . . 6
⊢ (∃y(B ∈ 𝐶 ∧ ψ) ↔
∃y(∃z ∈ 𝐶 z =
B ∧ ψ)) |
12 | 7, 8, 11 | 3bitr4ri 202 |
. . . . 5
⊢ (∃y(B ∈ 𝐶 ∧ ψ) ↔
∃z ∈ 𝐶 ∃y(z = B ∧ ψ)) |
13 | 5, 12 | bitri 173 |
. . . 4
⊢ (∃x(A ∈ 𝐶 ∧ φ) ↔
∃z ∈ 𝐶 ∃y(z = B ∧ ψ)) |
14 | | eqeq2 2046 |
. . . . . . . . . 10
⊢ (A = B →
(z = A
↔ z = B)) |
15 | 14 | imim2i 12 |
. . . . . . . . 9
⊢
((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
A = B)
→ (((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
(z = A
↔ z = B))) |
16 | | bi2 121 |
. . . . . . . . . . 11
⊢
((z = A ↔ z =
B) → (z = B →
z = A)) |
17 | 16 | imim2i 12 |
. . . . . . . . . 10
⊢
((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
(z = A
↔ z = B)) → (((A
∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
(z = B
→ z = A))) |
18 | | an31 498 |
. . . . . . . . . . . 12
⊢
((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) ∧ z = B) ↔ ((z =
B ∧
(B ∈
𝐶 ∧ ψ)) ∧ (A ∈ 𝐶 ∧ φ))) |
19 | 18 | imbi1i 227 |
. . . . . . . . . . 11
⊢
(((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) ∧ z = B) → z =
A) ↔ (((z = B ∧ (B ∈ 𝐶 ∧ ψ)) ∧
(A ∈
𝐶 ∧ φ)) →
z = A)) |
20 | | impexp 250 |
. . . . . . . . . . 11
⊢
(((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) ∧ z = B) → z =
A) ↔ (((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → (z = B →
z = A))) |
21 | | impexp 250 |
. . . . . . . . . . 11
⊢
((((z = B ∧ (B ∈ 𝐶 ∧ ψ)) ∧ (A ∈ 𝐶 ∧ φ)) → z = A) ↔
((z = B
∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))) |
22 | 19, 20, 21 | 3bitr3i 199 |
. . . . . . . . . 10
⊢
((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
(z = B
→ z = A)) ↔ ((z =
B ∧
(B ∈
𝐶 ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
23 | 17, 22 | sylib 127 |
. . . . . . . . 9
⊢
((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
(z = A
↔ z = B)) → ((z =
B ∧
(B ∈
𝐶 ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
24 | 15, 23 | syl 14 |
. . . . . . . 8
⊢
((((A ∈ 𝐶 ∧ φ) ∧
(B ∈
𝐶 ∧ ψ)) →
A = B)
→ ((z = B ∧ (B ∈ 𝐶 ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
25 | 24 | 2alimi 1342 |
. . . . . . 7
⊢ (∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) →
∀x∀y((z = B ∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))) |
26 | | 19.23v 1760 |
. . . . . . . . . 10
⊢ (∀y((z = B ∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))
↔ (∃y(z = B ∧ (B ∈ 𝐶 ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
27 | | an12 495 |
. . . . . . . . . . . . . 14
⊢
((z = B ∧ (B ∈ 𝐶 ∧ ψ)) ↔
(B ∈
𝐶 ∧ (z = B ∧ ψ))) |
28 | | eleq1 2097 |
. . . . . . . . . . . . . . . 16
⊢ (z = B →
(z ∈
𝐶 ↔ B ∈ 𝐶)) |
29 | 28 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢
((z = B ∧ ψ) → (z ∈ 𝐶 ↔ B ∈ 𝐶)) |
30 | 29 | pm5.32ri 428 |
. . . . . . . . . . . . . 14
⊢
((z ∈ 𝐶 ∧
(z = B
∧ ψ))
↔ (B ∈ 𝐶 ∧
(z = B
∧ ψ))) |
31 | 27, 30 | bitr4i 176 |
. . . . . . . . . . . . 13
⊢
((z = B ∧ (B ∈ 𝐶 ∧ ψ)) ↔
(z ∈
𝐶 ∧ (z = B ∧ ψ))) |
32 | 31 | exbii 1493 |
. . . . . . . . . . . 12
⊢ (∃y(z = B ∧ (B ∈ 𝐶 ∧ ψ)) ↔ ∃y(z ∈ 𝐶 ∧ (z = B ∧ ψ))) |
33 | | 19.42v 1783 |
. . . . . . . . . . . 12
⊢ (∃y(z ∈ 𝐶 ∧ (z = B ∧ ψ)) ↔ (z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ))) |
34 | 32, 33 | bitri 173 |
. . . . . . . . . . 11
⊢ (∃y(z = B ∧ (B ∈ 𝐶 ∧ ψ)) ↔ (z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ))) |
35 | 34 | imbi1i 227 |
. . . . . . . . . 10
⊢ ((∃y(z = B ∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))
↔ ((z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
36 | 26, 35 | bitri 173 |
. . . . . . . . 9
⊢ (∀y((z = B ∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))
↔ ((z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
37 | 36 | albii 1356 |
. . . . . . . 8
⊢ (∀x∀y((z = B ∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))
↔ ∀x((z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ)) →
((A ∈
𝐶 ∧ φ) →
z = A))) |
38 | | 19.21v 1750 |
. . . . . . . 8
⊢ (∀x((z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))
↔ ((z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ)) →
∀x((A ∈ 𝐶 ∧ φ) → z = A))) |
39 | 37, 38 | bitri 173 |
. . . . . . 7
⊢ (∀x∀y((z = B ∧ (B ∈ 𝐶 ∧ ψ)) → ((A ∈ 𝐶 ∧ φ) →
z = A))
↔ ((z ∈ 𝐶 ∧ ∃y(z = B ∧ ψ)) →
∀x((A ∈ 𝐶 ∧ φ) → z = A))) |
40 | 25, 39 | sylib 127 |
. . . . . 6
⊢ (∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) →
((z ∈
𝐶 ∧ ∃y(z = B ∧ ψ)) → ∀x((A ∈ 𝐶 ∧ φ) →
z = A))) |
41 | 40 | expd 245 |
. . . . 5
⊢ (∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) →
(z ∈
𝐶 → (∃y(z = B ∧ ψ) →
∀x((A ∈ 𝐶 ∧ φ) → z = A)))) |
42 | 41 | reximdvai 2413 |
. . . 4
⊢ (∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) →
(∃z
∈ 𝐶 ∃y(z = B ∧ ψ) →
∃z ∈ 𝐶 ∀x((A ∈ 𝐶 ∧ φ) →
z = A))) |
43 | 13, 42 | syl5bi 141 |
. . 3
⊢ (∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) →
(∃x(A ∈ 𝐶 ∧ φ) → ∃z ∈ 𝐶 ∀x((A ∈ 𝐶 ∧ φ) →
z = A))) |
44 | 43 | imp 115 |
. 2
⊢ ((∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) ∧ ∃x(A ∈ 𝐶 ∧ φ)) → ∃z ∈ 𝐶 ∀x((A ∈ 𝐶 ∧ φ) →
z = A)) |
45 | | pm4.24 375 |
. . . . . . . . 9
⊢
((A ∈ 𝐶 ∧ φ) ↔ ((A ∈ 𝐶 ∧ φ) ∧ (A ∈ 𝐶 ∧ φ))) |
46 | 45 | biimpi 113 |
. . . . . . . 8
⊢
((A ∈ 𝐶 ∧ φ) → ((A ∈ 𝐶 ∧ φ) ∧ (A ∈ 𝐶 ∧ φ))) |
47 | | prth 326 |
. . . . . . . 8
⊢
((((A ∈ 𝐶 ∧ φ) → z = A) ∧ ((A ∈ 𝐶 ∧ φ) → w = A)) →
(((A ∈
𝐶 ∧ φ) ∧ (A ∈ 𝐶 ∧ φ)) → (z = A ∧ w = A))) |
48 | | eqtr3 2056 |
. . . . . . . 8
⊢
((z = A ∧ w = A) →
z = w) |
49 | 46, 47, 48 | syl56 30 |
. . . . . . 7
⊢
((((A ∈ 𝐶 ∧ φ) → z = A) ∧ ((A ∈ 𝐶 ∧ φ) → w = A)) →
((A ∈
𝐶 ∧ φ) →
z = w)) |
50 | 49 | alanimi 1345 |
. . . . . 6
⊢ ((∀x((A ∈ 𝐶 ∧ φ) →
z = A)
∧ ∀x((A ∈ 𝐶 ∧ φ) →
w = A))
→ ∀x((A ∈ 𝐶 ∧ φ) → z = w)) |
51 | | 19.23v 1760 |
. . . . . . . 8
⊢ (∀x((A ∈ 𝐶 ∧ φ) →
z = w)
↔ (∃x(A ∈ 𝐶 ∧ φ) → z = w)) |
52 | 51 | biimpi 113 |
. . . . . . 7
⊢ (∀x((A ∈ 𝐶 ∧ φ) →
z = w)
→ (∃x(A ∈ 𝐶 ∧ φ) → z = w)) |
53 | 52 | com12 27 |
. . . . . 6
⊢ (∃x(A ∈ 𝐶 ∧ φ) →
(∀x((A ∈ 𝐶 ∧ φ) → z = w) →
z = w)) |
54 | 50, 53 | syl5 28 |
. . . . 5
⊢ (∃x(A ∈ 𝐶 ∧ φ) →
((∀x((A ∈ 𝐶 ∧ φ) → z = A) ∧ ∀x((A ∈ 𝐶 ∧ φ) → w = A)) →
z = w)) |
55 | 54 | a1d 22 |
. . . 4
⊢ (∃x(A ∈ 𝐶 ∧ φ) →
((z ∈
𝐶 ∧ w ∈ 𝐶) → ((∀x((A ∈ 𝐶 ∧ φ) →
z = A)
∧ ∀x((A ∈ 𝐶 ∧ φ) →
w = A))
→ z = w))) |
56 | 55 | ralrimivv 2394 |
. . 3
⊢ (∃x(A ∈ 𝐶 ∧ φ) →
∀z
∈ 𝐶 ∀w ∈ 𝐶 ((∀x((A ∈ 𝐶 ∧ φ) →
z = A)
∧ ∀x((A ∈ 𝐶 ∧ φ) →
w = A))
→ z = w)) |
57 | 56 | adantl 262 |
. 2
⊢ ((∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) ∧ ∃x(A ∈ 𝐶 ∧ φ)) → ∀z ∈ 𝐶 ∀w ∈ 𝐶 ((∀x((A ∈ 𝐶 ∧ φ) →
z = A)
∧ ∀x((A ∈ 𝐶 ∧ φ) →
w = A))
→ z = w)) |
58 | | eqeq1 2043 |
. . . . 5
⊢ (z = w →
(z = A
↔ w = A)) |
59 | 58 | imbi2d 219 |
. . . 4
⊢ (z = w →
(((A ∈
𝐶 ∧ φ) →
z = A)
↔ ((A ∈ 𝐶 ∧ φ) → w = A))) |
60 | 59 | albidv 1702 |
. . 3
⊢ (z = w →
(∀x((A ∈ 𝐶 ∧ φ) → z = A) ↔
∀x((A ∈ 𝐶 ∧ φ) → w = A))) |
61 | 60 | reu4 2729 |
. 2
⊢ (∃!z ∈ 𝐶 ∀x((A ∈ 𝐶 ∧ φ) →
z = A)
↔ (∃z ∈ 𝐶 ∀x((A ∈ 𝐶 ∧ φ) →
z = A)
∧ ∀z ∈ 𝐶 ∀w ∈ 𝐶 ((∀x((A ∈ 𝐶 ∧ φ) →
z = A)
∧ ∀x((A ∈ 𝐶 ∧ φ) →
w = A))
→ z = w))) |
62 | 44, 57, 61 | sylanbrc 394 |
1
⊢ ((∀x∀y(((A ∈ 𝐶 ∧ φ) ∧ (B ∈ 𝐶 ∧ ψ)) → A = B) ∧ ∃x(A ∈ 𝐶 ∧ φ)) → ∃!z ∈ 𝐶 ∀x((A ∈ 𝐶 ∧ φ) →
z = A)) |