Metamath Proof Explorer


Theorem intss2

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 A 𝒫 X A A X

Proof

Step Hyp Ref Expression
1 sspwuni A 𝒫 X A X
2 1 biimpi A 𝒫 X A X
3 intssuni A A A
4 sstr A A A X A X
5 4 expcom A X A A A X
6 2 3 5 syl2im A 𝒫 X A A X