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 | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | domssl | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω ) |