Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . . 4
⊢
Ⅎz(x ∈ A ∧ φ) |
2 | 1 | sb8eu 1910 |
. . 3
⊢ (∃!x(x ∈ A ∧ φ) ↔ ∃!z[z / x](x ∈ A ∧ φ)) |
3 | | sban 1826 |
. . . 4
⊢
([z / x](x ∈ A ∧ φ) ↔
([z / x]x ∈ A ∧ [z / x]φ)) |
4 | 3 | eubii 1906 |
. . 3
⊢ (∃!z[z / x](x ∈ A ∧ φ) ↔ ∃!z([z / x]x ∈ A ∧ [z / x]φ)) |
5 | | clelsb3 2139 |
. . . . . 6
⊢
([z / x]x ∈ A ↔
z ∈
A) |
6 | 5 | anbi1i 431 |
. . . . 5
⊢
(([z / x]x ∈ A ∧ [z / x]φ) ↔
(z ∈
A ∧
[z / x]φ)) |
7 | 6 | eubii 1906 |
. . . 4
⊢ (∃!z([z / x]x ∈ A ∧ [z / x]φ) ↔ ∃!z(z ∈ A ∧ [z / x]φ)) |
8 | | nfv 1418 |
. . . . . 6
⊢
Ⅎy z ∈ A |
9 | | cbvral.1 |
. . . . . . 7
⊢
Ⅎyφ |
10 | 9 | nfsb 1819 |
. . . . . 6
⊢
Ⅎy[z / x]φ |
11 | 8, 10 | nfan 1454 |
. . . . 5
⊢
Ⅎy(z ∈ A ∧ [z / x]φ) |
12 | | nfv 1418 |
. . . . 5
⊢
Ⅎz(y ∈ A ∧ ψ) |
13 | | eleq1 2097 |
. . . . . 6
⊢ (z = y →
(z ∈
A ↔ y ∈ A)) |
14 | | sbequ 1718 |
. . . . . . 7
⊢ (z = y →
([z / x]φ ↔
[y / x]φ)) |
15 | | cbvral.2 |
. . . . . . . 8
⊢
Ⅎxψ |
16 | | cbvral.3 |
. . . . . . . 8
⊢ (x = y →
(φ ↔ ψ)) |
17 | 15, 16 | sbie 1671 |
. . . . . . 7
⊢
([y / x]φ ↔
ψ) |
18 | 14, 17 | syl6bb 185 |
. . . . . 6
⊢ (z = y →
([z / x]φ ↔
ψ)) |
19 | 13, 18 | anbi12d 442 |
. . . . 5
⊢ (z = y →
((z ∈
A ∧
[z / x]φ) ↔
(y ∈
A ∧ ψ))) |
20 | 11, 12, 19 | cbveu 1921 |
. . . 4
⊢ (∃!z(z ∈ A ∧ [z / x]φ) ↔ ∃!y(y ∈ A ∧ ψ)) |
21 | 7, 20 | bitri 173 |
. . 3
⊢ (∃!z([z / x]x ∈ A ∧ [z / x]φ) ↔ ∃!y(y ∈ A ∧ ψ)) |
22 | 2, 4, 21 | 3bitri 195 |
. 2
⊢ (∃!x(x ∈ A ∧ φ) ↔ ∃!y(y ∈ A ∧ ψ)) |
23 | | df-reu 2307 |
. 2
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ)) |
24 | | df-reu 2307 |
. 2
⊢ (∃!y ∈ A ψ ↔ ∃!y(y ∈ A ∧ ψ)) |
25 | 22, 23, 24 | 3bitr4i 201 |
1
⊢ (∃!x ∈ A φ ↔ ∃!y ∈ A ψ) |