Theorem bj-nuliota

Description: Definition of the empty set using the definite description binder. See also bj-nuliotaALT . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2	1	eueqi	|- E! x x = (/)
3		eq0	|- ( x = (/) <-> A. y -. y e. x )
4	3	eubii	|- ( E! x x = (/) <-> E! x A. y -. y e. x )
5	2 4	mpbi	|- E! x A. y -. y e. x
6		eleq2	|- ( x = (/) -> ( y e. x <-> y e. (/) ) )
7	6	notbid	|- ( x = (/) -> ( -. y e. x <-> -. y e. (/) ) )
8	7	albidv	|- ( x = (/) -> ( A. y -. y e. x <-> A. y -. y e. (/) ) )
9	8	iota2	|- ( ( (/) e. _V /\ E! x A. y -. y e. x ) -> ( A. y -. y e. (/) <-> ( iota x A. y -. y e. x ) = (/) ) )
10	1 5 9	mp2an	|- ( A. y -. y e. (/) <-> ( iota x A. y -. y e. x ) = (/) )
11		noel	|- -. y e. (/)
12	10 11	mpgbi	|- ( iota x A. y -. y e. x ) = (/)
13	12	eqcomi	|- (/) = ( iota x A. y -. y e. x )