Proof of Theorem bj-axrep3
Step | Hyp | Ref
| Expression |
1 | | nfe1 2014 |
. . . 4
⊢
Ⅎ𝑦∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) |
2 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑦 𝑧 ∈ 𝑥 |
3 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑥 ∈ 𝑤 |
4 | | nfa1 2015 |
. . . . . . . 8
⊢
Ⅎ𝑦∀𝑦𝜑 |
5 | 3, 4 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑) |
6 | 5 | nfex 2140 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑) |
7 | 2, 6 | nfbi 1821 |
. . . . 5
⊢
Ⅎ𝑦(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) |
8 | 7 | nfal 2139 |
. . . 4
⊢
Ⅎ𝑦∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) |
9 | 1, 8 | nfim 1813 |
. . 3
⊢
Ⅎ𝑦(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) |
10 | 9 | nfex 2140 |
. 2
⊢
Ⅎ𝑦∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) |
11 | | elequ2 1991 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑤)) |
12 | 11 | anbi1d 737 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ((𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑) ↔ (𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) |
13 | 12 | exbidv 1837 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) |
14 | 13 | bibi2d 331 |
. . . . 5
⊢ (𝑦 = 𝑤 → ((𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)))) |
15 | 14 | albidv 1836 |
. . . 4
⊢ (𝑦 = 𝑤 → (∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)))) |
16 | 15 | imbi2d 329 |
. . 3
⊢ (𝑦 = 𝑤 → ((∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))))) |
17 | 16 | exbidv 1837 |
. 2
⊢ (𝑦 = 𝑤 → (∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))))) |
18 | | bj-axrep2 31977 |
. 2
⊢
∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
19 | 10, 17, 18 | bj-chvarv 31912 |
1
⊢
∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) |