Step |
Hyp |
Ref |
Expression |
1 |
|
cbvmowOLD.1 |
⊢ Ⅎ 𝑦 𝜑 |
2 |
|
cbvmowOLD.2 |
⊢ Ⅎ 𝑥 𝜓 |
3 |
|
cbvmowOLD.3 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
4 |
1
|
sb8ev |
⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) |
5 |
1
|
sb8euv |
⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) |
6 |
4 5
|
imbi12i |
⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) |
7 |
|
moeu |
⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ) |
8 |
|
moeu |
⊢ ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) |
9 |
6 7 8
|
3bitr4i |
⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) |
10 |
2 3
|
sbiev |
⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) |
11 |
10
|
mobii |
⊢ ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃* 𝑦 𝜓 ) |
12 |
9 11
|
bitri |
⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 ) |