This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssct

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 \subseteq B \land B ≼ ω) \to A ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		domssl	$⊢ (A \subseteq B \land B ≼ ω) \to A ≼ ω$