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 ⊢ φ → A ∈ V
unirestss.2 ⊢ φ → B ∈ W
Assertion unirestss ⊢ φ → ⋃ A ↾ 𝑡 B ⊆ ⋃ A

Proof

Step Hyp Ref Expression
1 unirestss.1 ⊢ φ → A ∈ V
2 unirestss.2 ⊢ φ → B ∈ W
3 1 2 restuni6 ⊢ φ → ⋃ A ↾ 𝑡 B = ⋃ A ∩ B
4 inss1 ⊢ ⋃ A ∩ B ⊆ ⋃ A
5 3 4 eqsstrdi ⊢ φ → ⋃ A ↾ 𝑡 B ⊆ ⋃ A