Theorem iunssd

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypothesis	iunssd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
Assertion	iunssd	$$⊢\phi \to \bigcup _{x\in A}B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		iunssd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
2	1	ralrimiva	$$⊢\phi \to \forall x\in AB\subseteq C$$
3		iunss	$$⊢\bigcup _{x\in A}B\subseteq C\leftrightarrow \forall x\in AB\subseteq C$$
4	2 3	sylibr	$$⊢\phi \to \bigcup _{x\in A}B\subseteq C$$