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	$$⊢\left(F\in \mathrm{fBas}\left(B\right)\wedge X\in F\right)\to X\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		fbsspw	$$⊢F\in \mathrm{fBas}\left(B\right)\to F\subseteq 𝒫B$$
2	1	sselda	$$⊢\left(F\in \mathrm{fBas}\left(B\right)\wedge X\in F\right)\to X\in 𝒫B$$
3	2	elpwid	$$⊢\left(F\in \mathrm{fBas}\left(B\right)\wedge X\in F\right)\to X\subseteq B$$