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

Metamath Proof Explorer

Theorem pinn

Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	pinn	$⊢ A \in 𝑵 \to A \in ω$

Step	Hyp	Ref	Expression
1		df-ni	$⊢ 𝑵 = ω ∖ \{\emptyset\}$
2		difss	$⊢ ω ∖ \{\emptyset\} \subseteq ω$
3	1 2	eqsstri	$⊢ 𝑵 \subseteq ω$
4	3	sseli	$⊢ A \in 𝑵 \to A \in ω$