Theorem iotaex

Description: Theorem 8.23 in Quine p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotaex	|- ( iota x ph ) e. _V

Proof

Step	Hyp	Ref	Expression
1		iotaval	|- ( A. x ( ph <-> x = z ) -> ( iota x ph ) = z )
2	1	eqcomd	|- ( A. x ( ph <-> x = z ) -> z = ( iota x ph ) )
3	2	eximi	|- ( E. z A. x ( ph <-> x = z ) -> E. z z = ( iota x ph ) )
4		eu6	|- ( E! x ph <-> E. z A. x ( ph <-> x = z ) )
5		isset	|- ( ( iota x ph ) e. _V <-> E. z z = ( iota x ph ) )
6	3 4 5	3imtr4i	|- ( E! x ph -> ( iota x ph ) e. _V )
7		iotanul	|- ( -. E! x ph -> ( iota x ph ) = (/) )
8		0ex	|- (/) e. _V
9	7 8	eqeltrdi	|- ( -. E! x ph -> ( iota x ph ) e. _V )
10	6 9	pm2.61i	|- ( iota x ph ) e. _V