Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | elisset 3215 |
. . . . 5
⊢ (𝐴 ∈ V → ∃𝑧 𝑧 = 𝐴) |
3 | 2 | 3ad2ant3 1084 |
. . . 4
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → ∃𝑧 𝑧 = 𝐴) |
4 | | nfnfc1 2767 |
. . . . . . 7
⊢
Ⅎ𝑥Ⅎ𝑥𝐴 |
5 | | nfcvd 2765 |
. . . . . . . 8
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝑧) |
6 | | id 22 |
. . . . . . . 8
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) |
7 | 5, 6 | nfeqd 2772 |
. . . . . . 7
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑧 = 𝐴) |
8 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴)) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢
(Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))) |
10 | 4, 7, 9 | cbvexd 2278 |
. . . . . 6
⊢
(Ⅎ𝑥𝐴 → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)) |
11 | 10 | ad2antrr 762 |
. . . . 5
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)) |
12 | 11 | 3adant3 1081 |
. . . 4
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)) |
13 | 3, 12 | mpbid 222 |
. . 3
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → ∃𝑥 𝑥 = 𝐴) |
14 | | biimp 205 |
. . . . . . . . 9
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
15 | 14 | imim2i 16 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜑 → 𝜓))) |
16 | 15 | com23 86 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜑 → (𝑥 = 𝐴 → 𝜓))) |
17 | 16 | imp 445 |
. . . . . 6
⊢ (((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝜑) → (𝑥 = 𝐴 → 𝜓)) |
18 | 17 | alanimi 1744 |
. . . . 5
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
19 | 18 | 3ad2ant2 1083 |
. . . 4
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
20 | | simp1r 1086 |
. . . . 5
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → Ⅎ𝑥𝜓) |
21 | | 19.23t 2079 |
. . . . 5
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
22 | 20, 21 | syl 17 |
. . . 4
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
23 | 19, 22 | mpbid 222 |
. . 3
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
24 | 13, 23 | mpd 15 |
. 2
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → 𝜓) |
25 | 1, 24 | syl3an3 1361 |
1
⊢
(((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) |