Theorem uniss2

Description: A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of TakeutiZaring p. 59. See iunss2 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004)

	Ref	Expression
Assertion	uniss2	$$⊢\forall x\in A\exists y\in Bx\subseteq y\to \bigcup A\subseteq \bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		ssuni	$$⊢\left(x\subseteq y\wedge y\in B\right)\to x\subseteq \bigcup B$$
2	1	expcom	$$⊢y\in B\to \left(x\subseteq y\to x\subseteq \bigcup B\right)$$
3	2	rexlimiv	$$⊢\exists y\in Bx\subseteq y\to x\subseteq \bigcup B$$
4	3	ralimi	$$⊢\forall x\in A\exists y\in Bx\subseteq y\to \forall x\in Ax\subseteq \bigcup B$$
5		unissb	$$⊢\bigcup A\subseteq \bigcup B\leftrightarrow \forall x\in Ax\subseteq \bigcup B$$
6	4 5	sylibr	$$⊢\forall x\in A\exists y\in Bx\subseteq y\to \bigcup A\subseteq \bigcup B$$