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 =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		al0ssb	$$⊢\forall yx\subseteq y\leftrightarrow x=\varnothing$$
3	2	ax-gen	$$⊢\forall x\left(\forall yx\subseteq y\leftrightarrow x=\varnothing \right)$$
4		eqeq2	$$⊢z=\varnothing \to \left(x=z\leftrightarrow x=\varnothing \right)$$
5	4	bibi2d	$$⊢z=\varnothing \to \left(\left(\forall yx\subseteq y\leftrightarrow x=z\right)\leftrightarrow \left(\forall yx\subseteq y\leftrightarrow x=\varnothing \right)\right)$$
6	5	albidv	$$⊢z=\varnothing \to \left(\forall x\left(\forall yx\subseteq y\leftrightarrow x=z\right)\leftrightarrow \forall x\left(\forall yx\subseteq y\leftrightarrow x=\varnothing \right)\right)$$
7		eqeq2	$$⊢z=\varnothing \to \left(\iota =z\leftrightarrow \iota =\varnothing \right)$$
8	6 7	imbi12d	$$⊢z=\varnothing \to \left(\left(\forall x\left(\forall yx\subseteq y\leftrightarrow x=z\right)\to \iota =z\right)\leftrightarrow \left(\forall x\left(\forall yx\subseteq y\leftrightarrow x=\varnothing \right)\to \iota =\varnothing \right)\right)$$
9		aiotaval	$$⊢\forall x\left(\forall yx\subseteq y\leftrightarrow x=z\right)\to \iota =z$$
10	8 9	vtoclg	$$⊢\varnothing \in \mathrm{V}\to \left(\forall x\left(\forall yx\subseteq y\leftrightarrow x=\varnothing \right)\to \iota =\varnothing \right)$$
11	1 3 10	mp2	$$⊢\iota =\varnothing$$