Theorem aiotaexb

Description: The alternate iota over a wff ph is a set iff there is a unique value x satisfying ph . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiotaexb	|- ( E! x ph <-> ( iota' x ph ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		intexab	|- ( E. y { x | ph } = { y } <-> |^| { y | { x | ph } = { y } } e. _V )
2		euabsn2	|- ( E! x ph <-> E. y { x | ph } = { y } )
3		df-aiota	|- ( iota' x ph ) = |^| { y | { x | ph } = { y } }
4	3	eleq1i	|- ( ( iota' x ph ) e. _V <-> |^| { y | { x | ph } = { y } } e. _V )
5	1 2 4	3bitr4i	|- ( E! x ph <-> ( iota' x ph ) e. _V )