Theorem bj-0nel1

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

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

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	nesymi	⊢ ¬ ∅ = 1o
3		0ex	⊢ ∅ ∈ V
4	3	elsn	⊢ ( ∅ ∈ { 1o } ↔ ∅ = 1o )
5	2 4	mtbir	⊢ ¬ ∅ ∈ { 1o }
6	5	nelir	⊢ ∅ ∉ { 1o }