Description: Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 7-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | ssct | |- ( ( A C_ B /\ B ~<_ _om ) -> A ~<_ _om ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | domssl | |- ( ( A C_ B /\ B ~<_ _om ) -> A ~<_ _om ) |