Subset of Set with Propositional Function

Theorem

Let $S$ be a set.

Let $P: S \to \set {\T, \F}$ be a propositional function on $S$.

Then:

$\set {x \in S: \map P x} \subseteq S$

Proof

 $\ds s$ $\in$ $\ds \set {x \in S: \map P x}$ $\ds \leadsto \ \$ $\ds s$ $\in$ $\ds \set {x \in S \land \map P x}$ $\ds \leadsto \ \$ $\ds s$ $\in$ $\ds \set {x \in S} \land \map P s$ Definition of Set Definition by Predicate $\ds \leadsto \ \$ $\ds s$ $\in$ $\ds \set {x \in S}$ Rule of Simplification $\ds \leadsto \ \$ $\ds s$ $\in$ $\ds S$ Definition of Element $\ds \leadsto \ \$ $\ds \set {x \in S: \map P x}$ $\subseteq$ $\ds S$ Definition of Subset

$\blacksquare$