Step | Hyp | Ref
| Expression |
1 | | simp3 1137 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑 ∧ 𝜑) → 𝜑) |
2 | | moi2.1 |
. . 3
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
3 | 1, 2 | syl5ibcom 244 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑 ∧ 𝜑) → (𝑥 = 𝐴 → 𝜓)) |
4 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜓 |
5 | 4, 2 | sbhypf 3490 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
6 | 5 | anbi2d 629 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜑 ∧ 𝜓))) |
7 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴)) |
8 | 6, 7 | imbi12d 345 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴))) |
9 | 8 | spcgv 3534 |
. . . . 5
⊢ (𝐴 ∈ 𝐵 → (∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴))) |
10 | | nfs1v 2153 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
11 | | sbequ12 2244 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
12 | 10, 11 | mo4f 2567 |
. . . . . 6
⊢
(∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
13 | | sp 2176 |
. . . . . 6
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
14 | 12, 13 | sylbi 216 |
. . . . 5
⊢
(∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
15 | 9, 14 | impel 506 |
. . . 4
⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴)) |
16 | 15 | expd 416 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑) → (𝜑 → (𝜓 → 𝑥 = 𝐴))) |
17 | 16 | 3impia 1116 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑 ∧ 𝜑) → (𝜓 → 𝑥 = 𝐴)) |
18 | 3, 17 | impbid 211 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ ∃*𝑥𝜑 ∧ 𝜑) → (𝑥 = 𝐴 ↔ 𝜓)) |