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

Metamath Proof Explorer

Theorem ssnum

Description: A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	ssnum	$⊢ (A \in dom card \land B \subseteq A) \to B \in dom card$

Step	Hyp	Ref	Expression
1		ssdomg	$⊢ A \in dom card \to (B \subseteq A \to B ≼ A)$
2	1	imp	$⊢ (A \in dom card \land B \subseteq A) \to B ≼ A$
3		numdom	$⊢ (A \in dom card \land B ≼ A) \to B \in dom card$
4	2 3	syldan	$⊢ (A \in dom card \land B \subseteq A) \to B \in dom card$