Subset of Set with Propositional Function

From ProofWiki
Jump to navigation Jump to search

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$


Sources