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 C_ ~P X -> ( A =/= (/) -> |^| A C_ X ) )

Proof

Step Hyp Ref Expression
1 sspwuni 
 |-  ( A C_ ~P X <-> U. A C_ X )
2 1 biimpi 
 |-  ( A C_ ~P X -> U. A C_ X )
3 intssuni 
 |-  ( A =/= (/) -> |^| A C_ U. A )
4 sstr 
 |-  ( ( |^| A C_ U. A /\ U. A C_ X ) -> |^| A C_ X )
5 4 expcom 
 |-  ( U. A C_ X -> ( |^| A C_ U. A -> |^| A C_ X ) )
6 2 3 5 syl2im 
 |-  ( A C_ ~P X -> ( A =/= (/) -> |^| A C_ X ) )