Theorem reuabaiotaiota

Description: The iota and the alternate iota over a wff ph are equal iff there is a unique satisfying value of { x | ph } = { y } . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	reuabaiotaiota	|- ( E! y { x | ph } = { y } <-> ( iota x ph ) = ( iota' x ph ) )

Proof

Step	Hyp	Ref	Expression
1		uniintab	|- ( E! y { x | ph } = { y } <-> U. { y | { x | ph } = { y } } = |^| { y | { x | ph } = { y } } )
2		df-iota	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
3		df-aiota	|- ( iota' x ph ) = |^| { y | { x | ph } = { y } }
4	2 3	eqeq12i	|- ( ( iota x ph ) = ( iota' x ph ) <-> U. { y | { x | ph } = { y } } = |^| { y | { x | ph } = { y } } )
5	1 4	bitr4i	|- ( E! y { x | ph } = { y } <-> ( iota x ph ) = ( iota' x ph ) )