# Metamath Proof Explorer

## Theorem aiotavb

Description: The alternate iota over a wff ph is the universe iff there is no unique value x satisfying ph . (Contributed by AV, 25-Aug-2022)

Ref Expression
Assertion aiotavb ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\iota =\mathrm{V}$

### Proof

Step Hyp Ref Expression
1 intnex ${⊢}¬\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}\in \mathrm{V}↔\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}=\mathrm{V}$
2 df-aiota ${⊢}\iota =\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}$
3 2 eleq1i ${⊢}\iota \in \mathrm{V}↔\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}\in \mathrm{V}$
4 3 notbii ${⊢}¬\iota \in \mathrm{V}↔¬\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}\in \mathrm{V}$
5 2 eqeq1i ${⊢}\iota =\mathrm{V}↔\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}=\mathrm{V}$
6 1 4 5 3bitr4i ${⊢}¬\iota \in \mathrm{V}↔\iota =\mathrm{V}$
7 aiotaexb ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\iota \in \mathrm{V}$
8 6 7 xchnxbir ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\iota =\mathrm{V}$