Theorem filsspw

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

	Ref	Expression
Assertion	filsspw	|- ( F e. ( Fil ` X ) -> F C_ ~P X )

Proof

Step	Hyp	Ref	Expression
1		filfbas	|- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2		fbsspw	|- ( F e. ( fBas ` X ) -> F C_ ~P X )
3	1 2	syl	|- ( F e. ( Fil ` X ) -> F C_ ~P X )