Theorem unirestss

Description: The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	unirestss.1	|- ( ph -> A e. V )
	unirestss.2	|- ( ph -> B e. W )
Assertion	unirestss	|- ( ph -> U. ( A |`t B ) C_ U. A )

Proof

Step	Hyp	Ref	Expression
1		unirestss.1	|- ( ph -> A e. V )
2		unirestss.2	|- ( ph -> B e. W )
3	1 2	restuni6	|- ( ph -> U. ( A |`t B ) = ( U. A i^i B ) )
4		inss1	|- ( U. A i^i B ) C_ U. A
5	3 4	eqsstrdi	|- ( ph -> U. ( A |`t B ) C_ U. A )