Can we prove without the axiom of choice that subspaces of finite dimensional vector spaces are finite dimensional as well? 
Let $E$ be a vector space and $F$ a subspace of $E$. 
  Show that if $E$ is finite dimensional then $F$ is finite dimensional too.

It's easy to prove by contradiction by taking a family linearly independent with $n+1$ vectors of $F$.
I can also prove it by using axiom of choice, I am curious if we can avoid axiom of choice to prove the result 'directly' (by directly I mean without using the method by contradiction)?
Thanks
 A: The usual proof (which you mentioned) doesn't use the axiom of choice at all.

You can prove this directly using induction. Pick some non-zero $w_1\in F$.
Suppose that we chose $w_1,\ldots,w_n$ and $F_n$ is their span. If $F_n=F$ then $F$ is finite dimensional. Otherwise, $F_n$ is a proper subspace of $F$, then we choose some $w_{n+1}\in F\setminus F_n$.
The induction stops at a stage which is at most $\dim E$, since the $w_i$'s are linearly independent. Since we only made finitely many choices, we didn't need to invoke the axiom of choice.
(Note that the proof doesn't cover the case $F=\{0\}$ but I'm sure you can manage proving this case on your own!)
A: Linear independence does not depend on which vector space you're in since $F\subseteq E$. By definition a basis is a maximal, linearly-independent, spanning set. Let $x_1,\ldots, x_n$ be any $n$ vectors in $F$. Then because they are also vectors in $E$ the maximal size of a linearly independent subset is $\text{dim}(F)$, hence $E$ has finite dimension by definition.
