Description: An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-restv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexr | ||
2 | 1 | adantl | |
3 | bj-restb | ||
4 | 2 3 | mpcom |