ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Definition D78
Subset
Formulation 0
Let $X$ be a D11: Set.
A D11: Set $E$ is a subset of $X$ if and only if \begin{equation} \forall \, x \in E : x \in X \end{equation}
Children
D80: Power set
D101: Proper subset
D954: Superset
Conventions
Convention 0 (Notation for subset relation)
If $X$ is a D11: Set and $E$ is a D78: Subset of $X$, we denote this by $E \subseteq X$.