Step | Hyp | Ref
| Expression |
1 | | elisset 3503 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴) |
2 | | nfnfc1 2977 |
. . . . . 6
⊢
Ⅎ𝑥Ⅎ𝑥𝐴 |
3 | | nfcvd 2975 |
. . . . . . 7
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝑧) |
4 | | id 22 |
. . . . . . 7
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) |
5 | 3, 4 | nfeqd 2985 |
. . . . . 6
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑧 = 𝐴) |
6 | | eqeq1 2822 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴)) |
7 | 6 | a1i 11 |
. . . . . 6
⊢
(Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))) |
8 | 2, 5, 7 | cbvexd 2420 |
. . . . 5
⊢
(Ⅎ𝑥𝐴 → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)) |
9 | 1, 8 | syl5ib 245 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)) |
10 | 9 | ad2antrr 722 |
. . 3
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)) |
11 | 10 | 3impia 1109 |
. 2
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → ∃𝑥 𝑥 = 𝐴) |
12 | | biimp 216 |
. . . . . . . . 9
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
13 | 12 | imim2i 16 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜑 → 𝜓))) |
14 | 13 | com23 86 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜑 → (𝑥 = 𝐴 → 𝜓))) |
15 | 14 | imp 407 |
. . . . . 6
⊢ (((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝜑) → (𝑥 = 𝐴 → 𝜓)) |
16 | 15 | alanimi 1808 |
. . . . 5
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
17 | | 19.23t 2200 |
. . . . . 6
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
18 | 17 | adantl 482 |
. . . . 5
⊢
((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
19 | 16, 18 | syl5ib 245 |
. . . 4
⊢
((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
20 | 19 | imp 407 |
. . 3
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
21 | 20 | 3adant3 1124 |
. 2
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
22 | 11, 21 | mpd 15 |
1
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) |