Theorem aiota0ndef

Description: Example for an undefined alternate iota being no set, i.e., A. y y e. x is a wff not satisfied by a (unique) value x (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef , where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiota0ndef	|- ( iota' x A. y y e. x ) e/ _V

Proof

Step	Hyp	Ref	Expression
1		nalset	|- -. E. x A. y y e. x
2	1	intnanr	|- -. ( E. x A. y y e. x /\ E* x A. y y e. x )
3		df-eu	|- ( E! x A. y y e. x <-> ( E. x A. y y e. x /\ E* x A. y y e. x ) )
4	2 3	mtbir	|- -. E! x A. y y e. x
5		df-nel	|- ( ( iota' x A. y y e. x ) e/ _V <-> -. ( iota' x A. y y e. x ) e. _V )
6		aiotaexb	|- ( E! x A. y y e. x <-> ( iota' x A. y y e. x ) e. _V )
7	5 6	xchbinxr	|- ( ( iota' x A. y y e. x ) e/ _V <-> -. E! x A. y y e. x )
8	4 7	mpbir	|- ( iota' x A. y y e. x ) e/ _V