Metamath Proof Explorer

Theorem elni

Description: Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion elni A 𝑵 A ω A


Step Hyp Ref Expression
1 df-ni 𝑵 = ω
2 1 eleq2i A 𝑵 A ω
3 eldifsn A ω A ω A
4 2 3 bitri A 𝑵 A ω A