Step |
Hyp |
Ref |
Expression |
1 |
|
intnex |
⊢ ( ¬ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = V ) |
2 |
|
df-aiota |
⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } |
3 |
2
|
eleq1i |
⊢ ( ( ℩' 𝑥 𝜑 ) ∈ V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V ) |
4 |
3
|
notbii |
⊢ ( ¬ ( ℩' 𝑥 𝜑 ) ∈ V ↔ ¬ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V ) |
5 |
2
|
eqeq1i |
⊢ ( ( ℩' 𝑥 𝜑 ) = V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = V ) |
6 |
1 4 5
|
3bitr4i |
⊢ ( ¬ ( ℩' 𝑥 𝜑 ) ∈ V ↔ ( ℩' 𝑥 𝜑 ) = V ) |
7 |
|
aiotaexb |
⊢ ( ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) ∈ V ) |
8 |
6 7
|
xchnxbir |
⊢ ( ¬ ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) = V ) |