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 ↔ ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) )