# Metamath Proof Explorer

## Theorem iotanul

Description: Theorem 8.22 in Quine p. 57. This theorem is the result if there isn't exactly one x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotanul ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 eu6 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)$
2 dfiota2 ${⊢}\left(\iota {x}|{\phi }\right)=\bigcup \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}$
3 alnex ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔¬\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)$
4 dfnul2 ${⊢}\varnothing =\left\{{z}|¬{z}={z}\right\}$
5 equid ${⊢}{z}={z}$
6 5 tbt ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔{z}={z}\right)$
7 6 biimpi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔{z}={z}\right)$
8 7 con1bid ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(¬{z}={z}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
9 8 alimi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(¬{z}={z}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
10 abbi1 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(¬{z}={z}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)\to \left\{{z}|¬{z}={z}\right\}=\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}$
11 9 10 syl ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left\{{z}|¬{z}={z}\right\}=\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}$
12 4 11 syl5req ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}=\varnothing$
13 3 12 sylbir ${⊢}¬\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}=\varnothing$
14 13 unieqd ${⊢}¬\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \bigcup \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}=\bigcup \varnothing$
15 uni0 ${⊢}\bigcup \varnothing =\varnothing$
16 14 15 syl6eq ${⊢}¬\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \bigcup \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}=\varnothing$
17 2 16 syl5eq ${⊢}¬\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(\iota {x}|{\phi }\right)=\varnothing$
18 1 17 sylnbi ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\varnothing$