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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	unirestss.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	unirestss	⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) ⊆ ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		unirestss.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		unirestss.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1 2	restuni6	⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 ) )
4		inss1	⊢ ( ∪ 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝐴
5	3 4	eqsstrdi	⊢ ( 𝜑 → ∪ ( 𝐴 ↾t 𝐵 ) ⊆ ∪ 𝐴 )