A theorem states that given an irreducible polynomial $f(x) \in F[x]$, the field $K = F[x]/(f(x))$ contains a root $\alpha$ of f(x).
The proof says that if we let $\alpha = \overline{x} \in F[x]/(f(x))$ then $f(\alpha) = \overline{f(x)} = 0$ so $\alpha$ is indeed a root of $f(x)$ in K.
The proof is what I don't understand - how is it valid? How does setting $\alpha = \overline{x}$ work? It is clear that $\overline{f(x)} = 0$, but how does this show that there exists a root (which is a constant) of f?
It's the equivalence class of the monomial $x$ in the quotient ring $K=F[x]/(f)$ where basically the element $f$ will be equal to $0$.
So, $f$ had no roots in the field $F$, but we want a (necessarily bigger) field where it has at least one root. And we do it by a construction: first we adjoin a formal element to $F$ - that's how $F[x]$ enters the picture, and then we force this new element to be a root of $f$, by taking the quotient.
In formulas, suppose $f=a_0+a_1x+a_2x^2+\dots$, and taking $\alpha:=\bar x$, we will have $$f(\alpha) = a_0+a_1\bar x+a_2\bar x^2+\dots=\overline{a_0+a_1x+a_2x^2+\dots}=\overline{f}=0$$ where in the middle we used that taking the quotient respects the ring operations.
Can you catch where we use that $f$ is irreducible?