Theorem unictb

Description: The countable union of countable sets is countable. Theorem 6Q of Enderton p. 159. See iunctb for indexed union version. (Contributed by NM, 26-Mar-2006)

	Ref	Expression
Assertion	unictb	|- ( ( A ~<_ _om /\ A. x e. A x ~<_ _om ) -> U. A ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		uniiun	|- U. A = U_ x e. A x
2		iunctb	|- ( ( A ~<_ _om /\ A. x e. A x ~<_ _om ) -> U_ x e. A x ~<_ _om )
3	1 2	eqbrtrid	|- ( ( A ~<_ _om /\ A. x e. A x ~<_ _om ) -> U. A ~<_ _om )