Theorem aiota0def

Description: Example for a defined alternate 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). This corresponds to iota0def . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiota0def	|- ( 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	ax-gen	|- A. x ( A. y x C_ y <-> x = (/) )
4		eqeq2	|- ( z = (/) -> ( x = z <-> x = (/) ) )
5	4	bibi2d	|- ( z = (/) -> ( ( A. y x C_ y <-> x = z ) <-> ( A. y x C_ y <-> x = (/) ) ) )
6	5	albidv	|- ( z = (/) -> ( A. x ( A. y x C_ y <-> x = z ) <-> A. x ( A. y x C_ y <-> x = (/) ) ) )
7		eqeq2	|- ( z = (/) -> ( ( iota' x A. y x C_ y ) = z <-> ( iota' x A. y x C_ y ) = (/) ) )
8	6 7	imbi12d	|- ( z = (/) -> ( ( A. x ( A. y x C_ y <-> x = z ) -> ( iota' x A. y x C_ y ) = z ) <-> ( A. x ( A. y x C_ y <-> x = (/) ) -> ( iota' x A. y x C_ y ) = (/) ) ) )
9		aiotaval	|- ( A. x ( A. y x C_ y <-> x = z ) -> ( iota' x A. y x C_ y ) = z )
10	8 9	vtoclg	|- ( (/) e. _V -> ( A. x ( A. y x C_ y <-> x = (/) ) -> ( iota' x A. y x C_ y ) = (/) ) )
11	1 3 10	mp2	|- ( iota' x A. y x C_ y ) = (/)