# Subset of Set with Propositional Function

## Theorem

Let $S$ be a set.

Let $P: S \to \set {\text{true}, \text{false} }$ be a propositional function on $S$.

Then:

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

## Proof

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

$\blacksquare$