Theorem bj-0nelsngl

Description: The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o ). (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-0nelsngl	$$⊢\varnothing \notin snglA$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	snnz	$$⊢\left\{x\right\}\ne \varnothing$$
3	2	nesymi	$$⊢\neg \varnothing =\left\{x\right\}$$
4	3	nex	$$⊢\neg \exists x\varnothing =\left\{x\right\}$$
5		bj-elsngl	$$⊢\varnothing \in snglA\leftrightarrow \exists x\in A\varnothing =\left\{x\right\}$$
6		rexex	$$⊢\exists x\in A\varnothing =\left\{x\right\}\to \exists x\varnothing =\left\{x\right\}$$
7	5 6	sylbi	$$⊢\varnothing \in snglA\to \exists x\varnothing =\left\{x\right\}$$
8	4 7	mto	$$⊢\neg \varnothing \in snglA$$
9	8	nelir	$$⊢\varnothing \notin snglA$$