Metamath Proof Explorer


Theorem elni2

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

Ref Expression
Assertion elni2 ( 𝐴N ↔ ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elni ( 𝐴N ↔ ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) )
2 nnord ( 𝐴 ∈ ω → Ord 𝐴 )
3 ord0eln0 ( Ord 𝐴 → ( ∅ ∈ 𝐴𝐴 ≠ ∅ ) )
4 2 3 syl ( 𝐴 ∈ ω → ( ∅ ∈ 𝐴𝐴 ≠ ∅ ) )
5 4 pm5.32i ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) )
6 1 5 bitr4i ( 𝐴N ↔ ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) )