Step |
Hyp |
Ref |
Expression |
1 |
|
eu6 |
⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) |
2 |
|
vex |
⊢ 𝑦 ∈ V |
3 |
2
|
intsn |
⊢ ∩ { 𝑦 } = 𝑦 |
4 |
|
abbi1 |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑦 } ) |
5 |
|
df-sn |
⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 } |
6 |
4 5
|
eqtr4di |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |
7 |
6
|
inteqd |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑦 } ) |
8 |
|
iotaval |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 ) |
9 |
3 7 8
|
3eqtr4a |
⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) ) |
10 |
9
|
exlimiv |
⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) ) |
11 |
1 10
|
sylbi |
⊢ ( ∃! 𝑥 𝜑 → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) ) |