Metamath Proof Explorer

Theorem bj-0nel1

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

Ref Expression
Assertion bj-0nel1 
|- (/) e/ { 1o }

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 1 nesymi 
 |-  -. (/) = 1o
3 0ex 
 |-  (/) e. _V
4 3 elsn 
 |-  ( (/) e. { 1o } <-> (/) = 1o )
5 2 4 mtbir 
 |-  -. (/) e. { 1o }
6 5 nelir 
 |-  (/) e/ { 1o }