Theorem iunssdf

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	iunssdf.1	$$⊢Ⅎx\phi$$
	iunssdf.2	$$⊢\underset{\_}{Ⅎ}xC$$
	iunssdf.3	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
Assertion	iunssdf	$$⊢\phi \to \bigcup _{x\in A}B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		iunssdf.1	$$⊢Ⅎx\phi$$
2		iunssdf.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		iunssdf.3	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
4	1 3	ralrimia	$$⊢\phi \to \forall x\in AB\subseteq C$$
5	2	iunssf	$$⊢\bigcup _{x\in A}B\subseteq C\leftrightarrow \forall x\in AB\subseteq C$$
6	4 5	sylibr	$$⊢\phi \to \bigcup _{x\in A}B\subseteq C$$