Theorem ssuniint

Description: Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	ssuniint.x	$$⊢Ⅎx\phi$$
	ssuniint.a	$$⊢\phi \to A\in V$$
	ssuniint.b	$$⊢\left(\phi \wedge x\in B\right)\to A\in x$$
Assertion	ssuniint	$$⊢\phi \to A\subseteq \bigcup \bigcap B$$

Proof

Step	Hyp	Ref	Expression
1		ssuniint.x	$$⊢Ⅎx\phi$$
2		ssuniint.a	$$⊢\phi \to A\in V$$
3		ssuniint.b	$$⊢\left(\phi \wedge x\in B\right)\to A\in x$$
4	1 2 3	elintd	$$⊢\phi \to A\in \bigcap B$$
5		elssuni	$$⊢A\in \bigcap B\to A\subseteq \bigcup \bigcap B$$
6	4 5	syl	$$⊢\phi \to A\subseteq \bigcup \bigcap B$$