Step | Hyp | Ref
| Expression |
1 | | elisset 2822 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴) |
2 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑧Ⅎ𝑥𝐴 |
3 | | nfnfc1 2912 |
. . . . . . . . 9
⊢
Ⅎ𝑥Ⅎ𝑥𝐴 |
4 | | nfcvd 2910 |
. . . . . . . . . . 11
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝑧) |
5 | | id 22 |
. . . . . . . . . . 11
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) |
6 | 4, 5 | nfeqd 2919 |
. . . . . . . . . 10
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑧 = 𝐴) |
7 | 6 | nfnd 1865 |
. . . . . . . . 9
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 ¬ 𝑧 = 𝐴) |
8 | | nfvd 1922 |
. . . . . . . . 9
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑧 ¬ 𝑥 = 𝐴) |
9 | | eqeq1 2744 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴)) |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
⊢
(Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))) |
11 | | notbi 319 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝐴 ↔ 𝑥 = 𝐴) ↔ (¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴)) |
12 | 10, 11 | syl6ib 250 |
. . . . . . . . . 10
⊢
(Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴))) |
13 | | biimp 214 |
. . . . . . . . . 10
⊢ ((¬
𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴) → (¬ 𝑧 = 𝐴 → ¬ 𝑥 = 𝐴)) |
14 | 12, 13 | syl6 35 |
. . . . . . . . 9
⊢
(Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (¬ 𝑧 = 𝐴 → ¬ 𝑥 = 𝐴))) |
15 | 2, 3, 7, 8, 14 | cbv1v 2337 |
. . . . . . . 8
⊢
(Ⅎ𝑥𝐴 → (∀𝑧 ¬ 𝑧 = 𝐴 → ∀𝑥 ¬ 𝑥 = 𝐴)) |
16 | | equcomi 2024 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → 𝑧 = 𝑥) |
17 | | biimpr 219 |
. . . . . . . . . 10
⊢ ((¬
𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴) → (¬ 𝑥 = 𝐴 → ¬ 𝑧 = 𝐴)) |
18 | 16, 12, 17 | syl56 36 |
. . . . . . . . 9
⊢
(Ⅎ𝑥𝐴 → (𝑥 = 𝑧 → (¬ 𝑥 = 𝐴 → ¬ 𝑧 = 𝐴))) |
19 | 3, 2, 8, 7, 18 | cbv1v 2337 |
. . . . . . . 8
⊢
(Ⅎ𝑥𝐴 → (∀𝑥 ¬ 𝑥 = 𝐴 → ∀𝑧 ¬ 𝑧 = 𝐴)) |
20 | 15, 19 | impbid 211 |
. . . . . . 7
⊢
(Ⅎ𝑥𝐴 → (∀𝑧 ¬ 𝑧 = 𝐴 ↔ ∀𝑥 ¬ 𝑥 = 𝐴)) |
21 | | alnex 1788 |
. . . . . . 7
⊢
(∀𝑧 ¬
𝑧 = 𝐴 ↔ ¬ ∃𝑧 𝑧 = 𝐴) |
22 | | alnex 1788 |
. . . . . . 7
⊢
(∀𝑥 ¬
𝑥 = 𝐴 ↔ ¬ ∃𝑥 𝑥 = 𝐴) |
23 | 20, 21, 22 | 3bitr3g 313 |
. . . . . 6
⊢
(Ⅎ𝑥𝐴 → (¬ ∃𝑧 𝑧 = 𝐴 ↔ ¬ ∃𝑥 𝑥 = 𝐴)) |
24 | 23 | con4bid 317 |
. . . . 5
⊢
(Ⅎ𝑥𝐴 → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)) |
25 | 1, 24 | syl5ib 243 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)) |
26 | 25 | ad2antrr 723 |
. . 3
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)) |
27 | 26 | 3impia 1116 |
. 2
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → ∃𝑥 𝑥 = 𝐴) |
28 | | biimp 214 |
. . . . . . . . 9
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
29 | 28 | imim2i 16 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜑 → 𝜓))) |
30 | 29 | com23 86 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜑 → (𝑥 = 𝐴 → 𝜓))) |
31 | 30 | imp 407 |
. . . . . 6
⊢ (((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝜑) → (𝑥 = 𝐴 → 𝜓)) |
32 | 31 | alanimi 1823 |
. . . . 5
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
33 | | 19.23t 2207 |
. . . . . 6
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
34 | 33 | adantl 482 |
. . . . 5
⊢
((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
35 | 32, 34 | syl5ib 243 |
. . . 4
⊢
((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
36 | 35 | imp 407 |
. . 3
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
37 | 36 | 3adant3 1131 |
. 2
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
38 | 27, 37 | mpd 15 |
1
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) |