Theorem bj-0nel1

Description: The empty set does not belong to { 1o } . (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-0nel1	$$⊢\varnothing \notin \left\{1_{𝑜}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2	1	nesymi	$$⊢\neg \varnothing =1_{𝑜}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3	elsn	$$⊢\varnothing \in \left\{1_{𝑜}\right\}\leftrightarrow \varnothing =1_{𝑜}$$
5	2 4	mtbir	$$⊢\neg \varnothing \in \left\{1_{𝑜}\right\}$$
6	5	nelir	$$⊢\varnothing \notin \left\{1_{𝑜}\right\}$$