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 ) = (/) )