# 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
`|- ( -. E! x ph -> ( iota x ph ) = (/) )`

### Proof

Step Hyp Ref Expression
1 eu6
` |-  ( E! x ph <-> E. z A. x ( ph <-> x = z ) )`
2 dfiota2
` |-  ( iota x ph ) = U. { z | A. x ( ph <-> x = z ) }`
3 alnex
` |-  ( A. z -. A. x ( ph <-> x = z ) <-> -. E. z A. x ( ph <-> x = z ) )`
4 dfnul2
` |-  (/) = { z | -. z = z }`
5 equid
` |-  z = z`
6 5 tbt
` |-  ( -. A. x ( ph <-> x = z ) <-> ( -. A. x ( ph <-> x = z ) <-> z = z ) )`
7 6 biimpi
` |-  ( -. A. x ( ph <-> x = z ) -> ( -. A. x ( ph <-> x = z ) <-> z = z ) )`
8 7 con1bid
` |-  ( -. A. x ( ph <-> x = z ) -> ( -. z = z <-> A. x ( ph <-> x = z ) ) )`
9 8 alimi
` |-  ( A. z -. A. x ( ph <-> x = z ) -> A. z ( -. z = z <-> A. x ( ph <-> x = z ) ) )`
10 abbi1
` |-  ( A. z ( -. z = z <-> A. x ( ph <-> x = z ) ) -> { z | -. z = z } = { z | A. x ( ph <-> x = z ) } )`
11 9 10 syl
` |-  ( A. z -. A. x ( ph <-> x = z ) -> { z | -. z = z } = { z | A. x ( ph <-> x = z ) } )`
12 4 11 syl5req
` |-  ( A. z -. A. x ( ph <-> x = z ) -> { z | A. x ( ph <-> x = z ) } = (/) )`
13 3 12 sylbir
` |-  ( -. E. z A. x ( ph <-> x = z ) -> { z | A. x ( ph <-> x = z ) } = (/) )`
14 13 unieqd
` |-  ( -. E. z A. x ( ph <-> x = z ) -> U. { z | A. x ( ph <-> x = z ) } = U. (/) )`
15 uni0
` |-  U. (/) = (/)`
16 14 15 eqtrdi
` |-  ( -. E. z A. x ( ph <-> x = z ) -> U. { z | A. x ( ph <-> x = z ) } = (/) )`
17 2 16 syl5eq
` |-  ( -. E. z A. x ( ph <-> x = z ) -> ( iota x ph ) = (/) )`
18 1 17 sylnbi
` |-  ( -. E! x ph -> ( iota x ph ) = (/) )`