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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unirestss.1 | |
|
2 | unirestss.2 | |
|
3 | 1 2 | restuni6 | |
4 | inss1 | |
|
5 | 3 4 | eqsstrdi | |