ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Subset
Definition D101
Proper subset
Formulation 0
Let $X$ be a D11: Set.
A D11: Set $E$ is a proper subset of $X$ if and only if
(1) $\forall \, x \in E : x \in X$ (D78: Subset)
(2) $E \neq X$
Conventions
Convention 0 (Notation for proper subset relation)
If $X$ is a D11: Set and $E$ is a D101: Proper subset of $X$, we denote this by $E \subset X$.