Theorem aiotavb

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

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

Proof

Step	Hyp	Ref	Expression
1		intnex	|- ( -. |^| { y | { x | ph } = { y } } e. _V <-> |^| { y | { x | ph } = { y } } = _V )
2		df-aiota	|- ( iota' x ph ) = |^| { y | { x | ph } = { y } }
3	2	eleq1i	|- ( ( iota' x ph ) e. _V <-> |^| { y | { x | ph } = { y } } e. _V )
4	3	notbii	|- ( -. ( iota' x ph ) e. _V <-> -. |^| { y | { x | ph } = { y } } e. _V )
5	2	eqeq1i	|- ( ( iota' x ph ) = _V <-> |^| { y | { x | ph } = { y } } = _V )
6	1 4 5	3bitr4i	|- ( -. ( iota' x ph ) e. _V <-> ( iota' x ph ) = _V )
7		aiotaexb	|- ( E! x ph <-> ( iota' x ph ) e. _V )
8	6 7	xchnxbir	|- ( -. E! x ph <-> ( iota' x ph ) = _V )