Description: A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | intss2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sspwuni | ||
2 | 1 | biimpi | |
3 | intssuni | ||
4 | sstr | ||
5 | 4 | expcom | |
6 | 2 3 5 | syl2im |