This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in 𝑵 \leftrightarrow (A \in ω \land A \neq \emptyset)$

Step	Hyp	Ref	Expression
1		df-ni	$⊢ 𝑵 = ω ∖ \{\emptyset\}$
2	1	eleq2i	$⊢ A \in 𝑵 \leftrightarrow A \in (ω ∖ \{\emptyset\})$
3		eldifsn	$⊢ A \in (ω ∖ \{\emptyset\}) \leftrightarrow (A \in ω \land A \neq \emptyset)$
4	2 3	bitri	$⊢ A \in 𝑵 \leftrightarrow (A \in ω \land A \neq \emptyset)$