Proof of Theorem reu6
Step | Hyp | Ref
| Expression |
1 | | df-reu 2307 |
. 2
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ)) |
2 | | 19.28v 1777 |
. . . . 5
⊢ (∀x(y ∈ A ∧ (x ∈ A → (φ
↔ x = y))) ↔ (y
∈ A ∧ ∀x(x ∈ A →
(φ ↔ x = y)))) |
3 | | eleq1 2097 |
. . . . . . . . . . . 12
⊢ (x = y →
(x ∈
A ↔ y ∈ A)) |
4 | | sbequ12 1651 |
. . . . . . . . . . . 12
⊢ (x = y →
(φ ↔ [y / x]φ)) |
5 | 3, 4 | anbi12d 442 |
. . . . . . . . . . 11
⊢ (x = y →
((x ∈
A ∧ φ) ↔ (y ∈ A ∧ [y / x]φ))) |
6 | | equequ1 1595 |
. . . . . . . . . . 11
⊢ (x = y →
(x = y
↔ y = y)) |
7 | 5, 6 | bibi12d 224 |
. . . . . . . . . 10
⊢ (x = y →
(((x ∈
A ∧ φ) ↔ x = y) ↔
((y ∈
A ∧
[y / x]φ) ↔
y = y))) |
8 | | equid 1586 |
. . . . . . . . . . . 12
⊢ y = y |
9 | 8 | tbt 236 |
. . . . . . . . . . 11
⊢
((y ∈ A ∧ [y / x]φ) ↔
((y ∈
A ∧
[y / x]φ) ↔
y = y)) |
10 | | simpl 102 |
. . . . . . . . . . 11
⊢
((y ∈ A ∧ [y / x]φ) →
y ∈
A) |
11 | 9, 10 | sylbir 125 |
. . . . . . . . . 10
⊢
(((y ∈ A ∧ [y / x]φ) ↔
y = y)
→ y ∈ A) |
12 | 7, 11 | syl6bi 152 |
. . . . . . . . 9
⊢ (x = y →
(((x ∈
A ∧ φ) ↔ x = y) →
y ∈
A)) |
13 | 12 | spimv 1689 |
. . . . . . . 8
⊢ (∀x((x ∈ A ∧ φ) ↔ x = y) →
y ∈
A) |
14 | | bi1 111 |
. . . . . . . . . . . 12
⊢
(((x ∈ A ∧ φ) ↔
x = y)
→ ((x ∈ A ∧ φ) →
x = y)) |
15 | 14 | expdimp 246 |
. . . . . . . . . . 11
⊢
((((x ∈ A ∧ φ) ↔
x = y)
∧ x ∈ A) →
(φ → x = y)) |
16 | | bi2 121 |
. . . . . . . . . . . . 13
⊢
(((x ∈ A ∧ φ) ↔
x = y)
→ (x = y → (x
∈ A ∧ φ))) |
17 | | simpr 103 |
. . . . . . . . . . . . 13
⊢
((x ∈ A ∧ φ) →
φ) |
18 | 16, 17 | syl6 29 |
. . . . . . . . . . . 12
⊢
(((x ∈ A ∧ φ) ↔
x = y)
→ (x = y → φ)) |
19 | 18 | adantr 261 |
. . . . . . . . . . 11
⊢
((((x ∈ A ∧ φ) ↔
x = y)
∧ x ∈ A) →
(x = y
→ φ)) |
20 | 15, 19 | impbid 120 |
. . . . . . . . . 10
⊢
((((x ∈ A ∧ φ) ↔
x = y)
∧ x ∈ A) →
(φ ↔ x = y)) |
21 | 20 | ex 108 |
. . . . . . . . 9
⊢
(((x ∈ A ∧ φ) ↔
x = y)
→ (x ∈ A →
(φ ↔ x = y))) |
22 | 21 | sps 1427 |
. . . . . . . 8
⊢ (∀x((x ∈ A ∧ φ) ↔ x = y) →
(x ∈
A → (φ ↔ x = y))) |
23 | 13, 22 | jca 290 |
. . . . . . 7
⊢ (∀x((x ∈ A ∧ φ) ↔ x = y) →
(y ∈
A ∧
(x ∈
A → (φ ↔ x = y)))) |
24 | 23 | a5i 1432 |
. . . . . 6
⊢ (∀x((x ∈ A ∧ φ) ↔ x = y) →
∀x(y ∈ A ∧ (x ∈ A →
(φ ↔ x = y)))) |
25 | | bi1 111 |
. . . . . . . . . . 11
⊢ ((φ ↔ x = y) →
(φ → x = y)) |
26 | 25 | imim2i 12 |
. . . . . . . . . 10
⊢
((x ∈ A →
(φ ↔ x = y)) →
(x ∈
A → (φ → x = y))) |
27 | 26 | impd 242 |
. . . . . . . . 9
⊢
((x ∈ A →
(φ ↔ x = y)) →
((x ∈
A ∧ φ) → x = y)) |
28 | 27 | adantl 262 |
. . . . . . . 8
⊢
((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) →
((x ∈
A ∧ φ) → x = y)) |
29 | | eleq1a 2106 |
. . . . . . . . . . . 12
⊢ (y ∈ A → (x =
y → x ∈ A)) |
30 | 29 | adantr 261 |
. . . . . . . . . . 11
⊢
((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) →
(x = y
→ x ∈ A)) |
31 | 30 | imp 115 |
. . . . . . . . . 10
⊢
(((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) ∧ x = y) → x
∈ A) |
32 | | bi2 121 |
. . . . . . . . . . . . . 14
⊢ ((φ ↔ x = y) →
(x = y
→ φ)) |
33 | 32 | imim2i 12 |
. . . . . . . . . . . . 13
⊢
((x ∈ A →
(φ ↔ x = y)) →
(x ∈
A → (x = y →
φ))) |
34 | 33 | com23 72 |
. . . . . . . . . . . 12
⊢
((x ∈ A →
(φ ↔ x = y)) →
(x = y
→ (x ∈ A →
φ))) |
35 | 34 | imp 115 |
. . . . . . . . . . 11
⊢
(((x ∈ A →
(φ ↔ x = y)) ∧ x = y) → (x
∈ A
→ φ)) |
36 | 35 | adantll 445 |
. . . . . . . . . 10
⊢
(((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) ∧ x = y) → (x
∈ A
→ φ)) |
37 | 31, 36 | jcai 294 |
. . . . . . . . 9
⊢
(((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) ∧ x = y) → (x
∈ A ∧ φ)) |
38 | 37 | ex 108 |
. . . . . . . 8
⊢
((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) →
(x = y
→ (x ∈ A ∧ φ))) |
39 | 28, 38 | impbid 120 |
. . . . . . 7
⊢
((y ∈ A ∧ (x ∈ A →
(φ ↔ x = y))) →
((x ∈
A ∧ φ) ↔ x = y)) |
40 | 39 | alimi 1341 |
. . . . . 6
⊢ (∀x(y ∈ A ∧ (x ∈ A → (φ
↔ x = y))) → ∀x((x ∈ A ∧ φ) ↔ x = y)) |
41 | 24, 40 | impbii 117 |
. . . . 5
⊢ (∀x((x ∈ A ∧ φ) ↔ x = y) ↔
∀x(y ∈ A ∧ (x ∈ A →
(φ ↔ x = y)))) |
42 | | df-ral 2305 |
. . . . . 6
⊢ (∀x ∈ A (φ ↔ x = y) ↔
∀x(x ∈ A →
(φ ↔ x = y))) |
43 | 42 | anbi2i 430 |
. . . . 5
⊢
((y ∈ A ∧ ∀x ∈ A (φ ↔
x = y))
↔ (y ∈ A ∧ ∀x(x ∈ A →
(φ ↔ x = y)))) |
44 | 2, 41, 43 | 3bitr4i 201 |
. . . 4
⊢ (∀x((x ∈ A ∧ φ) ↔ x = y) ↔
(y ∈
A ∧ ∀x ∈ A (φ ↔ x = y))) |
45 | 44 | exbii 1493 |
. . 3
⊢ (∃y∀x((x ∈ A ∧ φ) ↔ x = y) ↔
∃y(y ∈ A ∧ ∀x ∈ A (φ ↔
x = y))) |
46 | | df-eu 1900 |
. . 3
⊢ (∃!x(x ∈ A ∧ φ) ↔ ∃y∀x((x ∈ A ∧ φ) ↔ x = y)) |
47 | | df-rex 2306 |
. . 3
⊢ (∃y ∈ A ∀x ∈ A (φ ↔ x = y) ↔
∃y(y ∈ A ∧ ∀x ∈ A (φ ↔
x = y))) |
48 | 45, 46, 47 | 3bitr4i 201 |
. 2
⊢ (∃!x(x ∈ A ∧ φ) ↔ ∃y ∈ A ∀x ∈ A (φ ↔ x = y)) |
49 | 1, 48 | bitri 173 |
1
⊢ (∃!x ∈ A φ ↔ ∃y ∈ A ∀x ∈ A (φ ↔ x = y)) |