Theorem dfaiota2

Description: Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in Quine p. 56. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	dfaiota2	|- ( iota' x ph ) = |^| { y | A. x ( ph <-> x = y ) }

Proof

Step	Hyp	Ref	Expression
1		df-aiota	|- ( iota' x ph ) = |^| { 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	inteqi	|- |^| { y | { x | ph } = { y } } = |^| { y | A. x ( ph <-> x = y ) }
5	1 4	eqtri	|- ( iota' x ph ) = |^| { y | A. x ( ph <-> x = y ) }