Theorem bj-1nel0

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

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

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2	1	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
3		elsni	$$⊢1_{𝑜}\in \left\{\varnothing \right\}\to 1_{𝑜}=\varnothing$$
4	2 3	mto	$$⊢\neg 1_{𝑜}\in \left\{\varnothing \right\}$$
5	4	nelir	$$⊢1_{𝑜}\notin \left\{\varnothing \right\}$$