This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 abbi 
 |-  ( 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 eqtr2id 
 |-  ( 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 eqtrid 
 |-  ( -. E. z A. x ( ph <-> x = z ) -> ( iota x ph ) = (/) )
18 1 17 sylnbi 
 |-  ( -. E! x ph -> ( iota x ph ) = (/) )