Metamath Proof Explorer

Theorem ondif1

Description: Two ways to say that A is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion ondif1 
|- ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )

Proof

Step Hyp Ref Expression
1 dif1o 
 |-  ( A e. ( On \ 1o ) <-> ( A e. On /\ A =/= (/) ) )
2 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
3 2 pm5.32i 
 |-  ( ( A e. On /\ (/) e. A ) <-> ( A e. On /\ A =/= (/) ) )
4 1 3 bitr4i 
 |-  ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )