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

Metamath Proof Explorer

Theorem elnn

Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998)

		Ref	Expression
	Assertion	elnn	$⊢ (A \in B \land B \in ω) \to A \in ω$

Step	Hyp	Ref	Expression
1		trom	$⊢ Tr ω$
2		trel	$⊢ Tr ω \to ((A \in B \land B \in ω) \to A \in ω)$
3	1 2	ax-mp	$⊢ (A \in B \land B \in ω) \to A \in ω$