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	$$⊢\varnothing =\left(\iota x|\forall y\neg y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \left(\iota x|\forall y\neg y\in x\right)$$
2		iotassuni	$$⊢\left(\iota x|\forall y\neg y\in x\right)\subseteq \bigcup \left\{x|\forall y\neg y\in x\right\}$$
3		eq0	$$⊢x=\varnothing \leftrightarrow \forall y\neg y\in x$$
4	3	bicomi	$$⊢\forall y\neg y\in x\leftrightarrow x=\varnothing$$
5	4	abbii	$$⊢\left\{x|\forall y\neg y\in x\right\}=\left\{x|x=\varnothing \right\}$$
6	5	unieqi	$$⊢\bigcup \left\{x|\forall y\neg y\in x\right\}=\bigcup \left\{x|x=\varnothing \right\}$$
7		df-sn	$$⊢\left\{\varnothing \right\}=\left\{x|x=\varnothing \right\}$$
8	7	eqcomi	$$⊢\left\{x|x=\varnothing \right\}=\left\{\varnothing \right\}$$
9	8	unieqi	$$⊢\bigcup \left\{x|x=\varnothing \right\}=\bigcup \left\{\varnothing \right\}$$
10		0ex	$$⊢\varnothing \in \mathrm{V}$$
11	10	unisn	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$
12	6 9 11	3eqtri	$$⊢\bigcup \left\{x|\forall y\neg y\in x\right\}=\varnothing$$
13	2 12	sseqtri	$$⊢\left(\iota x|\forall y\neg y\in x\right)\subseteq \varnothing$$
14	1 13	eqssi	$$⊢\varnothing =\left(\iota x|\forall y\neg y\in x\right)$$