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 e. dom card /\ B C_ A ) -> B e. dom card )

Proof

Step Hyp Ref Expression
1 ssdomg 
 |-  ( A e. dom card -> ( B C_ A -> B ~<_ A ) )
2 1 imp 
 |-  ( ( A e. dom card /\ B C_ A ) -> B ~<_ A )
3 numdom 
 |-  ( ( A e. dom card /\ B ~<_ A ) -> B e. dom card )
4 2 3 syldan 
 |-  ( ( A e. dom card /\ B C_ A ) -> B e. dom card )