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	|- F/ x ph
	ssuniint.a	|- ( ph -> A e. V )
	ssuniint.b	|- ( ( ph /\ x e. B ) -> A e. x )
Assertion	ssuniint	|- ( ph -> A C_ U. |^| B )

Proof

Step	Hyp	Ref	Expression
1		ssuniint.x	|- F/ x ph
2		ssuniint.a	|- ( ph -> A e. V )
3		ssuniint.b	|- ( ( ph /\ x e. B ) -> A e. x )
4	1 2 3	elintd	|- ( ph -> A e. |^| B )
5		elssuni	|- ( A e. |^| B -> A C_ U. |^| B )
6	4 5	syl	|- ( ph -> A C_ U. |^| B )