Theorem iota0def

Description: Example for a defined iota being the empty set, i.e., A. y x C_ y is a wff satisfied by a unique value x , namely x = (/) (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	iota0def	|- ( iota x A. y x C_ y ) = (/)

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		al0ssb	|- ( A. y x C_ y <-> x = (/) )
3	2	a1i	|- ( ( (/) e. _V /\ (/) e. _V ) -> ( A. y x C_ y <-> x = (/) ) )
4	3	iota5	|- ( ( (/) e. _V /\ (/) e. _V ) -> ( iota x A. y x C_ y ) = (/) )
5	1 1 4	mp2an	|- ( iota x A. y x C_ y ) = (/)