This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) ⊆ ∪ 𝐴 )