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

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

Step	Hyp	Ref	Expression
1		elni	$⊢ A \in 𝑵 \leftrightarrow (A \in ω \land A \neq \emptyset)$
2		nnord	$⊢ A \in ω \to Ord A$
3		ord0eln0	$⊢ Ord A \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
4	2 3	syl	$⊢ A \in ω \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
5	4	pm5.32i	$⊢ (A \in ω \land \emptyset \in A) \leftrightarrow (A \in ω \land A \neq \emptyset)$
6	1 5	bitr4i	$⊢ A \in 𝑵 \leftrightarrow (A \in ω \land \emptyset \in A)$