Step |
Hyp |
Ref |
Expression |
1 |
|
findes.1 |
⊢ [ ∅ / 𝑥 ] 𝜑 |
2 |
|
findes.2 |
⊢ ( 𝑥 ∈ ω → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ) |
3 |
|
dfsbcq2 |
⊢ ( 𝑧 = ∅ → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ ∅ / 𝑥 ] 𝜑 ) ) |
4 |
|
sbequ |
⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) |
5 |
|
dfsbcq2 |
⊢ ( 𝑧 = suc 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ suc 𝑦 / 𝑥 ] 𝜑 ) ) |
6 |
|
sbequ12r |
⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) |
7 |
|
nfv |
⊢ Ⅎ 𝑥 𝑦 ∈ ω |
8 |
|
nfs1v |
⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 |
9 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ suc 𝑦 / 𝑥 ] 𝜑 |
10 |
8 9
|
nfim |
⊢ Ⅎ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) |
11 |
7 10
|
nfim |
⊢ Ⅎ 𝑥 ( 𝑦 ∈ ω → ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) ) |
12 |
|
eleq1w |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ω ↔ 𝑦 ∈ ω ) ) |
13 |
|
sbequ12 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) |
14 |
|
suceq |
⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 ) |
15 |
14
|
sbceq1d |
⊢ ( 𝑥 = 𝑦 → ( [ suc 𝑥 / 𝑥 ] 𝜑 ↔ [ suc 𝑦 / 𝑥 ] 𝜑 ) ) |
16 |
13 15
|
imbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) ) ) |
17 |
12 16
|
imbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ω → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ) ↔ ( 𝑦 ∈ ω → ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) ) ) ) |
18 |
11 17 2
|
chvarfv |
⊢ ( 𝑦 ∈ ω → ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) ) |
19 |
3 4 5 6 1 18
|
finds |
⊢ ( 𝑥 ∈ ω → 𝜑 ) |