Step |
Hyp |
Ref |
Expression |
1 |
|
nfe1 |
⊢ Ⅎ 𝑦 ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) |
2 |
|
nfv |
⊢ Ⅎ 𝑦 𝑧 ∈ 𝑥 |
3 |
|
nfv |
⊢ Ⅎ 𝑦 𝑥 ∈ 𝑤 |
4 |
|
nfa1 |
⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑 |
5 |
3 4
|
nfan |
⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) |
6 |
5
|
nfex |
⊢ Ⅎ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) |
7 |
2 6
|
nfbi |
⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) |
8 |
7
|
nfal |
⊢ Ⅎ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) |
9 |
1 8
|
nfim |
⊢ Ⅎ 𝑦 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) |
10 |
9
|
nfex |
⊢ Ⅎ 𝑦 ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) |
11 |
|
axreplem |
⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) ) ) |
12 |
|
axrep2 |
⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) |
13 |
10 11 12
|
chvarfv |
⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) |