Metamath Proof Explorer


Theorem el1o

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

Ref Expression
Assertion el1o A 1 𝑜 A =

Proof

Step Hyp Ref Expression
1 df1o2 1 𝑜 =
2 1 eleq2i A 1 𝑜 A
3 0ex V
4 3 elsn2 A A =
5 2 4 bitri A 1 𝑜 A =