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 φAV
unirestss.2 φBW
Assertion unirestss φA𝑡BA

Proof

Step Hyp Ref Expression
1 unirestss.1 φAV
2 unirestss.2 φBW
3 1 2 restuni6 φA𝑡B=AB
4 inss1 ABA
5 3 4 eqsstrdi φA𝑡BA