Metamath Proof Explorer

Theorem el1o

Description: Membership in ordinal one. (Contributed by NM, 5-Jan-2005)

Ref Expression
Assertion el1o 
|- ( A e. 1o <-> A = (/) )

Proof

Step Hyp Ref Expression
1 df1o2 
 |-  1o = { (/) }
2 1 eleq2i 
 |-  ( A e. 1o <-> A e. { (/) } )
3 0ex 
 |-  (/) e. _V
4 3 elsn2 
 |-  ( A e. { (/) } <-> A = (/) )
5 2 4 bitri 
 |-  ( A e. 1o <-> A = (/) )