Theorem dfiota2

Description: Alternate definition for descriptions. Definition 8.18 in Quine p. 56. (Contributed by Andrew Salmon, 30-Jun-2011)

	Ref	Expression
Assertion	dfiota2	|- ( iota x ph ) = U. { y | A. x ( ph <-> x = y ) }

Proof

Step	Hyp	Ref	Expression
1		df-iota	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
2		absn	|- ( { x | ph } = { y } <-> A. x ( ph <-> x = y ) )
3	2	abbii	|- { y | { x | ph } = { y } } = { y | A. x ( ph <-> x = y ) }
4	3	unieqi	|- U. { y | { x | ph } = { y } } = U. { y | A. x ( ph <-> x = y ) }
5	1 4	eqtri	|- ( iota x ph ) = U. { y | A. x ( ph <-> x = y ) }