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	$$⊢\phi \to A\in V$$
	unirestss.2	$$⊢\phi \to B\in W$$
Assertion	unirestss	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)\subseteq \bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		unirestss.1	$$⊢\phi \to A\in V$$
2		unirestss.2	$$⊢\phi \to B\in W$$
3	1 2	restuni6	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)=\bigcup A\cap B$$
4		inss1	$$⊢\bigcup A\cap B\subseteq \bigcup A$$
5	3 4	eqsstrdi	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)\subseteq \bigcup A$$