Step |
Hyp |
Ref |
Expression |
1 |
|
eusnsn |
⊢ ∃! 𝑧 { 𝑧 } = { 𝑦 } |
2 |
|
eqcom |
⊢ ( { 𝑦 } = { 𝑧 } ↔ { 𝑧 } = { 𝑦 } ) |
3 |
2
|
eubii |
⊢ ( ∃! 𝑧 { 𝑦 } = { 𝑧 } ↔ ∃! 𝑧 { 𝑧 } = { 𝑦 } ) |
4 |
1 3
|
mpbir |
⊢ ∃! 𝑧 { 𝑦 } = { 𝑧 } |
5 |
|
eqeq1 |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ { 𝑦 } = { 𝑧 } ) ) |
6 |
5
|
eubidv |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ ∃! 𝑧 { 𝑦 } = { 𝑧 } ) ) |
7 |
4 6
|
mpbiri |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ) |
8 |
|
absn |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) |
9 |
|
reuabaiotaiota |
⊢ ( ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) ) |
10 |
|
eqcom |
⊢ ( ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) ↔ ( ℩' 𝑥 𝜑 ) = ( ℩ 𝑥 𝜑 ) ) |
11 |
9 10
|
bitri |
⊢ ( ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ ( ℩' 𝑥 𝜑 ) = ( ℩ 𝑥 𝜑 ) ) |
12 |
7 8 11
|
3imtr3i |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩' 𝑥 𝜑 ) = ( ℩ 𝑥 𝜑 ) ) |
13 |
|
iotaval |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 ) |
14 |
12 13
|
eqtrd |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩' 𝑥 𝜑 ) = 𝑦 ) |