Description: Two ways to say that A is a nonzero ordinal number. Lemma 1.10 of Schloeder p. 2. (Contributed by Mario Carneiro, 21-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ondif1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dif1o | ||
2 | on0eln0 | ||
3 | 2 | pm5.32i | |
4 | 1 3 | bitr4i |