Description: Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | elni2 | ⊢ ( 𝐴 ∈ N ↔ ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ) |
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 ↔ ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ) |