Metamath Proof Explorer

Theorem nnne0s

Description: A surreal positive integer is non-zero. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion nnne0s 
|- ( A e. NN_s -> A =/= 0s )

Proof

Step Hyp Ref Expression
1 eldifsni 
 |-  ( A e. ( NN0_s \ { 0s } ) -> A =/= 0s )
2 df-nns 
 |-  NN_s = ( NN0_s \ { 0s } )
3 1 2 eleq2s 
 |-  ( A e. NN_s -> A =/= 0s )