Step | Hyp | Ref
| Expression |
1 | | simp3 957 |
. . 3
⊢ ((A ∈ B ∧ ∃*xφ ∧ φ) → φ) |
2 | | moi2.1 |
. . 3
⊢ (x = A →
(φ ↔ ψ)) |
3 | 1, 2 | syl5ibcom 211 |
. 2
⊢ ((A ∈ B ∧ ∃*xφ ∧ φ) → (x = A →
ψ)) |
4 | | nfs1v 2106 |
. . . . . . . 8
⊢ Ⅎx[y / x]φ |
5 | | sbequ12 1919 |
. . . . . . . 8
⊢ (x = y →
(φ ↔ [y / x]φ)) |
6 | 4, 5 | mo4f 2236 |
. . . . . . 7
⊢ (∃*xφ ↔ ∀x∀y((φ ∧
[y / x]φ) →
x = y)) |
7 | | sp 1747 |
. . . . . . 7
⊢ (∀x∀y((φ ∧
[y / x]φ) →
x = y)
→ ∀y((φ ∧ [y / x]φ) →
x = y)) |
8 | 6, 7 | sylbi 187 |
. . . . . 6
⊢ (∃*xφ → ∀y((φ ∧
[y / x]φ) →
x = y)) |
9 | | nfv 1619 |
. . . . . . . . . 10
⊢ Ⅎxψ |
10 | 9, 2 | sbhypf 2904 |
. . . . . . . . 9
⊢ (y = A →
([y / x]φ ↔
ψ)) |
11 | 10 | anbi2d 684 |
. . . . . . . 8
⊢ (y = A →
((φ ∧
[y / x]φ) ↔
(φ ∧
ψ))) |
12 | | eqeq2 2362 |
. . . . . . . 8
⊢ (y = A →
(x = y
↔ x = A)) |
13 | 11, 12 | imbi12d 311 |
. . . . . . 7
⊢ (y = A →
(((φ ∧
[y / x]φ) →
x = y)
↔ ((φ ∧ ψ) →
x = A))) |
14 | 13 | spcgv 2939 |
. . . . . 6
⊢ (A ∈ B → (∀y((φ ∧
[y / x]φ) →
x = y)
→ ((φ ∧ ψ) →
x = A))) |
15 | 8, 14 | syl5 28 |
. . . . 5
⊢ (A ∈ B → (∃*xφ → ((φ ∧ ψ) → x = A))) |
16 | 15 | imp 418 |
. . . 4
⊢ ((A ∈ B ∧ ∃*xφ) → ((φ ∧ ψ) → x = A)) |
17 | 16 | exp3a 425 |
. . 3
⊢ ((A ∈ B ∧ ∃*xφ) → (φ → (ψ → x = A))) |
18 | 17 | 3impia 1148 |
. 2
⊢ ((A ∈ B ∧ ∃*xφ ∧ φ) → (ψ → x = A)) |
19 | 3, 18 | impbid 183 |
1
⊢ ((A ∈ B ∧ ∃*xφ ∧ φ) → (x = A ↔
ψ)) |