Metamath Proof Explorer

Theorem bj-1nel0

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

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

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 1 neii 
 |-  -. 1o = (/)
3 elsni 
 |-  ( 1o e. { (/) } -> 1o = (/) )
4 2 3 mto 
 |-  -. 1o e. { (/) }
5 4 nelir 
 |-  1o e/ { (/) }