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) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 23-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		abbi	|- ( A. x ( ph <-> x = y ) -> { x | ph } = { x | x = y } )
2		df-sn	|- { y } = { x | x = y }
3	1 2	eqtr4di	|- ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )
4		iotaval2	|- ( { x | ph } = { y } -> ( iota x ph ) = y )
5	3 4	syl	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )