Let $V$ be a vector space. $B\subseteq V$ is a basis of $V$ if $B$ spans $V$ and is linearly independent.
The length of a basis is its cardinality.
BS#PROP-EXT. Basis Extension. $\lrimp\AC$
Let $V$ be a vector space. For any linearly independent subset $S\subseteq V$, there is a basis $B\supseteq S$.
BS#PROP-SEL. Basis Selection. $\lrimp\AC$
Let $V$ be a vector space. For any spanning subset $S\subseteq V$, there is a basis $B\subseteq S$.
BS#PROP-EX. Existence of Basis. $\lrimp\AC$
Every vector space has a basis.
BS#PROP-ST. Steinitz Exchange Lemma.
Let $V$ be a vector space. If $A\subseteq V$ is linearly independent and $B\subseteq V$ spans $V$, then there is a set $T\subseteq A$ with $\lvert T\rvert=\lvert B\rvert-\lvert A\rvert$ such that $A\sqcup T$ spans $V$.
All bases of a vector space have the same length.