Theorem bj-nuliotaALT

Description: Alternate proof of bj-nuliota . Note that this alternate proof uses the fact that iota x ph evaluates to (/) when there is no x satisfying ph ( iotanul ). This is an implementation detail of the encoding currently used in set.mm and should be avoided. (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-nuliotaALT	|- (/) = ( iota x A. y -. y e. x )

Proof

Step	Hyp	Ref	Expression
1		0ss	|- (/) C_ ( iota x A. y -. y e. x )
2		iotassuni	|- ( iota x A. y -. y e. x ) C_ U. { x | A. y -. y e. x }
3		eq0	|- ( x = (/) <-> A. y -. y e. x )
4	3	bicomi	|- ( A. y -. y e. x <-> x = (/) )
5	4	abbii	|- { x | A. y -. y e. x } = { x | x = (/) }
6	5	unieqi	|- U. { x | A. y -. y e. x } = U. { x | x = (/) }
7		df-sn	|- { (/) } = { x | x = (/) }
8	7	eqcomi	|- { x | x = (/) } = { (/) }
9	8	unieqi	|- U. { x | x = (/) } = U. { (/) }
10		0ex	|- (/) e. _V
11	10	unisn	|- U. { (/) } = (/)
12	6 9 11	3eqtri	|- U. { x | A. y -. y e. x } = (/)
13	2 12	sseqtri	|- ( iota x A. y -. y e. x ) C_ (/)
14	1 13	eqssi	|- (/) = ( iota x A. y -. y e. x )