Theorem iotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotaval	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )

Proof

Step	Hyp	Ref	Expression
1		dfiota2	|- ( iota x ph ) = U. { z | A. x ( ph <-> x = z ) }
2		sbeqalb	|- ( y e. _V -> ( ( A. x ( ph <-> x = y ) /\ A. x ( ph <-> x = z ) ) -> y = z ) )
3	2	elv	|- ( ( A. x ( ph <-> x = y ) /\ A. x ( ph <-> x = z ) ) -> y = z )
4	3	ex	|- ( A. x ( ph <-> x = y ) -> ( A. x ( ph <-> x = z ) -> y = z ) )
5		equequ2	|- ( y = z -> ( x = y <-> x = z ) )
6	5	bibi2d	|- ( y = z -> ( ( ph <-> x = y ) <-> ( ph <-> x = z ) ) )
7	6	biimpd	|- ( y = z -> ( ( ph <-> x = y ) -> ( ph <-> x = z ) ) )
8	7	alimdv	|- ( y = z -> ( A. x ( ph <-> x = y ) -> A. x ( ph <-> x = z ) ) )
9	8	com12	|- ( A. x ( ph <-> x = y ) -> ( y = z -> A. x ( ph <-> x = z ) ) )
10	4 9	impbid	|- ( A. x ( ph <-> x = y ) -> ( A. x ( ph <-> x = z ) <-> y = z ) )
11		equcom	|- ( y = z <-> z = y )
12	10 11	bitrdi	|- ( A. x ( ph <-> x = y ) -> ( A. x ( ph <-> x = z ) <-> z = y ) )
13	12	alrimiv	|- ( A. x ( ph <-> x = y ) -> A. z ( A. x ( ph <-> x = z ) <-> z = y ) )
14		uniabio	|- ( A. z ( A. x ( ph <-> x = z ) <-> z = y ) -> U. { z | A. x ( ph <-> x = z ) } = y )
15	13 14	syl	|- ( A. x ( ph <-> x = y ) -> U. { z | A. x ( ph <-> x = z ) } = y )
16	1 15	eqtrid	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )