Metamath Proof Explorer

Theorem fbelss

Description: An element of the filter base is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbelss 
|- ( ( F e. ( fBas ` B ) /\ X e. F ) -> X C_ B )

Proof

Step Hyp Ref Expression
1 fbsspw 
 |-  ( F e. ( fBas ` B ) -> F C_ ~P B )
2 1 sselda 
 |-  ( ( F e. ( fBas ` B ) /\ X e. F ) -> X e. ~P B )
3 2 elpwid 
 |-  ( ( F e. ( fBas ` B ) /\ X e. F ) -> X C_ B )