Theorem nosgnn0i

Description: If X is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011)

	Ref	Expression
Hypothesis	nosgnn0i.1	|- X e. { 1o , 2o }
Assertion	nosgnn0i	|- (/) =/= X

Proof

Step	Hyp	Ref	Expression
1		nosgnn0i.1	|- X e. { 1o , 2o }
2		nosgnn0	|- -. (/) e. { 1o , 2o }
3		eleq1	|- ( (/) = X -> ( (/) e. { 1o , 2o } <-> X e. { 1o , 2o } ) )
4	1 3	mpbiri	|- ( (/) = X -> (/) e. { 1o , 2o } )
5	2 4	mto	|- -. (/) = X
6	5	neir	|- (/) =/= X