Theorem bj-1nel0

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

	Ref	Expression
Assertion	bj-1nel0	⊢ 1o ∉ { ∅ }

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	neii	⊢ ¬ 1o = ∅
3		elsni	⊢ ( 1o ∈ { ∅ } → 1o = ∅ )
4	2 3	mto	⊢ ¬ 1o ∈ { ∅ }
5	4	nelir	⊢ 1o ∉ { ∅ }