Step |
Hyp |
Ref |
Expression |
1 |
|
axrep4.1 |
⊢ Ⅎ 𝑧 𝜑 |
2 |
|
axrep3 |
⊢ ∃ 𝑥 ( ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ) |
3 |
2
|
19.35i |
⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ) |
4 |
|
nfv |
⊢ Ⅎ 𝑧 𝑦 ∈ 𝑥 |
5 |
|
nfv |
⊢ Ⅎ 𝑧 𝑥 ∈ 𝑤 |
6 |
|
nfa1 |
⊢ Ⅎ 𝑧 ∀ 𝑧 𝜑 |
7 |
5 6
|
nfan |
⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) |
8 |
7
|
nfex |
⊢ Ⅎ 𝑧 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) |
9 |
4 8
|
nfbi |
⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) |
10 |
9
|
nfal |
⊢ Ⅎ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) |
11 |
|
nfv |
⊢ Ⅎ 𝑥 𝑦 ∈ 𝑧 |
12 |
|
nfe1 |
⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) |
13 |
11 12
|
nfbi |
⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
14 |
13
|
nfal |
⊢ Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
15 |
|
elequ2 |
⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 ) ) |
16 |
1
|
19.3 |
⊢ ( ∀ 𝑧 𝜑 ↔ 𝜑 ) |
17 |
16
|
anbi2i |
⊢ ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
18 |
17
|
exbii |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
19 |
18
|
a1i |
⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) |
20 |
15 19
|
bibi12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) ) |
21 |
20
|
albidv |
⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) ) |
22 |
10 14 21
|
cbvexv1 |
⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) |
23 |
3 22
|
sylib |
⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) |