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 ( ( 𝐴 ∈ 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 )