Theorem aiotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022)

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

Proof

Step	Hyp	Ref	Expression
1		eusnsn	|- E! z { z } = { y }
2		eqcom	|- ( { y } = { z } <-> { z } = { y } )
3	2	eubii	|- ( E! z { y } = { z } <-> E! z { z } = { y } )
4	1 3	mpbir	|- E! z { y } = { z }
5		eqeq1	|- ( { x | ph } = { y } -> ( { x | ph } = { z } <-> { y } = { z } ) )
6	5	eubidv	|- ( { x | ph } = { y } -> ( E! z { x | ph } = { z } <-> E! z { y } = { z } ) )
7	4 6	mpbiri	|- ( { x | ph } = { y } -> E! z { x | ph } = { z } )
8		absn	|- ( { x | ph } = { y } <-> A. x ( ph <-> x = y ) )
9		reuabaiotaiota	|- ( E! z { x | ph } = { z } <-> ( iota x ph ) = ( iota' x ph ) )
10		eqcom	|- ( ( iota x ph ) = ( iota' x ph ) <-> ( iota' x ph ) = ( iota x ph ) )
11	9 10	bitri	|- ( E! z { x | ph } = { z } <-> ( iota' x ph ) = ( iota x ph ) )
12	7 8 11	3imtr3i	|- ( A. x ( ph <-> x = y ) -> ( iota' x ph ) = ( iota x ph ) )
13		iotaval	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
14	12 13	eqtrd	|- ( A. x ( ph <-> x = y ) -> ( iota' x ph ) = y )