Step |
Hyp |
Ref |
Expression |
1 |
|
sb8eulem.nfsb |
⊢ Ⅎ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 |
2 |
|
sb8v |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑤 [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ) |
3 |
|
equsb3 |
⊢ ( [ 𝑤 / 𝑥 ] 𝑥 = 𝑧 ↔ 𝑤 = 𝑧 ) |
4 |
3
|
sblbis |
⊢ ( [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝑤 = 𝑧 ) ) |
5 |
4
|
albii |
⊢ ( ∀ 𝑤 [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑤 ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝑤 = 𝑧 ) ) |
6 |
|
nfv |
⊢ Ⅎ 𝑦 𝑤 = 𝑧 |
7 |
1 6
|
nfbi |
⊢ Ⅎ 𝑦 ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝑤 = 𝑧 ) |
8 |
|
nfv |
⊢ Ⅎ 𝑤 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) |
9 |
|
sbequ |
⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) |
10 |
|
equequ1 |
⊢ ( 𝑤 = 𝑦 → ( 𝑤 = 𝑧 ↔ 𝑦 = 𝑧 ) ) |
11 |
9 10
|
bibi12d |
⊢ ( 𝑤 = 𝑦 → ( ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝑤 = 𝑧 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) ) ) |
12 |
7 8 11
|
cbvalv1 |
⊢ ( ∀ 𝑤 ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝑤 = 𝑧 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) ) |
13 |
2 5 12
|
3bitri |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) ) |
14 |
13
|
exbii |
⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) ) |
15 |
|
eu6 |
⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) |
16 |
|
eu6 |
⊢ ( ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑧 ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) ) |
17 |
14 15 16
|
3bitr4i |
⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) |