Step |
Hyp |
Ref |
Expression |
1 |
|
nfe1 |
⊢ Ⅎ 𝑤 ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) |
2 |
|
nfv |
⊢ Ⅎ 𝑤 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) |
3 |
1 2
|
nfim |
⊢ Ⅎ 𝑤 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) |
4 |
3
|
nfex |
⊢ Ⅎ 𝑤 ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) |
5 |
|
axreplem |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) ) |
6 |
|
axrep1 |
⊢ ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) |
7 |
4 5 6
|
chvarfv |
⊢ ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) |
8 |
|
sp |
⊢ ( ∀ 𝑦 𝜑 → 𝜑 ) |
9 |
8
|
imim1i |
⊢ ( ( 𝜑 → 𝑧 = 𝑦 ) → ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
10 |
9
|
alimi |
⊢ ( ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
11 |
10
|
eximi |
⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
12 |
|
nfv |
⊢ Ⅎ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) |
13 |
|
nfa1 |
⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑 |
14 |
|
nfv |
⊢ Ⅎ 𝑦 𝑧 = 𝑤 |
15 |
13 14
|
nfim |
⊢ Ⅎ 𝑦 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) |
16 |
15
|
nfal |
⊢ Ⅎ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) |
17 |
|
equequ2 |
⊢ ( 𝑦 = 𝑤 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝑤 ) ) |
18 |
17
|
imbi2d |
⊢ ( 𝑦 = 𝑤 → ( ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) ) ) |
19 |
18
|
albidv |
⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) ) ) |
20 |
12 16 19
|
cbvexv1 |
⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) ) |
21 |
11 20
|
sylib |
⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) ) |
22 |
21
|
imim1i |
⊢ ( ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) → ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
23 |
7 22
|
eximii |
⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) |