Step |
Hyp |
Ref |
Expression |
1 |
|
elequ2 |
⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) ) |
2 |
1
|
anbi1d |
⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) |
3 |
2
|
exbidv |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) |
4 |
3
|
bibi2d |
⊢ ( 𝑤 = 𝑦 → ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) ) |
5 |
4
|
albidv |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) ) |
6 |
5
|
exbidv |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) ) |
7 |
6
|
imbi2d |
⊢ ( 𝑤 = 𝑦 → ( ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) ↔ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) ) ) |
8 |
|
ax-rep |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) |
9 |
|
19.3v |
⊢ ( ∀ 𝑦 𝜑 ↔ 𝜑 ) |
10 |
9
|
imbi1i |
⊢ ( ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) ) |
11 |
10
|
albii |
⊢ ( ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) |
12 |
11
|
exbii |
⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) |
13 |
12
|
albii |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) |
14 |
|
nfv |
⊢ Ⅎ 𝑥 𝑧 ∈ 𝑦 |
15 |
|
nfe1 |
⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) |
16 |
14 15
|
nfbi |
⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) |
17 |
16
|
nfal |
⊢ Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) |
18 |
|
nfv |
⊢ Ⅎ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
19 |
|
elequ2 |
⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ) ) |
20 |
9
|
anbi2i |
⊢ ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
21 |
20
|
exbii |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) |
22 |
21
|
a1i |
⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) |
23 |
19 22
|
bibi12d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) ) |
24 |
23
|
albidv |
⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) ) |
25 |
17 18 24
|
cbvexv1 |
⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) |
26 |
8 13 25
|
3imtr3i |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) |
27 |
7 26
|
chvarvv |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) |
28 |
27
|
19.35ri |
⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) |