Theorem ssnum

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

	Ref	Expression
Assertion	ssnum	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		ssdomg	⊢ ( 𝐴 ∈ dom card → ( 𝐵 ⊆ 𝐴 → 𝐵 ≼ 𝐴 ) )
2	1	imp	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ≼ 𝐴 )
3		numdom	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card )
4	2 3	syldan	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ dom card )