I have seen a few questions about the constructions of quotients of smooth vector bundles on StackExchange, but I don't think any of them provides a completely satisfactory answer.
I would like to summarize my questions as follows.
Since we don't often use the explicit construction of quotient bundles, what are the most important properties of quotient bundles that we use in practice?
If you've seen a good and self-contained construction of quotient bundles, I would be happy to know, so please feel free to list the reference.
I propose the following construction of quotient bundles, does it make sense?
Let $F\subseteq E$ be a subbundle over $X$, where $\operatorname{rank}F=r$, and $\operatorname{rank}E=k$.
As the total space, we define $E/F$ to be $E/_\sim$, equipped with the quotient topology, where $\sim$ is the equivalence on $E$ defined by $u\sim v$ if and only if $u$ and $v$ live over the same fiber $E_x$ and $u-v\in F_x$. Note that $$ \tilde\pi^{-1}(U)=\pi_E^{-1}(U)/_\sim, $$ where $\sim$ is the same equivalence relation described above.
We need local trivializations on $E/F$. Let $q\in X$. Consider an open set $q\in U\subseteq X$ over which both $E$ and $F$ are trivial. Then the following diagram $$ U \times\mathbb{R}^r \longleftarrow \pi_F^{-1}(U) \stackrel{\subseteq}{\longrightarrow} \pi_E^{-1}(U) \longrightarrow U\times\mathbb{R}^k $$ commutes over $U$, where the left and right arrows are local trivializations. By composing the three arrows, we obtain, for each $x\in U$, a linear map $B(x):\mathbb{R}^r\to\mathbb{R}^k$, i.e., a $k\times r$ matrix. Furthermore, $B(x)$ depends smoothly on $x$ and is injective for all $x\in U$. Without loss of generality, assume that the first $r$ rows of $B(q)$ are linearly independent, so the top $r\times r$ minor of $B(q)$ has a nonzero determinant. By shrinking $U$ if necessary, we may assume that the top $r\times r$ minor of $B(x)$ has a nonzero determinant for all $x\in U$.
Now note that the matrix $$ \left(\begin{array}{c|c} B(x)_{r\times r} & O \\ \hline B(x)_{(k-r)\times r} & I_{k-r} \end{array}\right) $$ has a nonzero determinant. Let $W\subseteq\mathbb{R}^k$ be the subspace spanned by $e_{r+1},\ldots,e_k$. Since the above matrix is invertible, we have $\mathbb{R}^k=\operatorname{Im}B(x)\oplus W$ for all $x\in U$. Hence, for each $x\in U$, there is a projection $\pi_x:\mathbb{R}^k\to W$ whose kernel is $\operatorname{Im}B(x)$.
Now consider the map $$ \require{AMScd} \begin{CD} \pi_E^{-1}(U) @>>> U\times\mathbb{R}^k @>~(x,v)~\mapsto~(x,\pi_x(v))~>> U\times W, \end{CD} $$ where the first arrow is just the trivialization of $E$ over $U$. Then the composite map is constant on the equivalence classes of $\sim$ in $\pi_E^{-1}(U)$, so it induces a map $$ \require{AMScd} \begin{CD} \pi_E^{-1}(U)/_\sim=\tilde\pi^{-1}(U) @>>> U\times W \end{CD} $$ which is the desired local trivialization. And now one probably needs to do some more checkings to ensure everything is compatible, but this is the basic idea.
Here's one way: First, let $E/F$ be the disjoint union of the vector spaces $E_x/F_x$ for each $x \in X$. Then given any section $s$ of $E$, there is a naturally defined map $$ [s]: X \rightarrow E/F,$$ where $$[s](x) = [s(x)].$$ The space of smooth sections of $E/F$ is the $C^\infty(X)$-module generated by these maps. This uniquely determines the vector bundle structure.
Here is a more concrete way to explain this: At each $x_0 \in X$, choose a basis $(s_1(x_0), \dots, s_k(x_0))$ of $E_x$ such that $(s_1(x_0), \dots, s_r(x_0))$ is a basis of $F_x$. This can be extended to a local frame in a neighborhood of $x_0$ such that the sections $(s_{r+1}, \dots, s_k)$ span a $(k-r)$-dimensional subbundle pointiwse transversak to $F$. This then defines a local frame $([s_{r+1}], \dots, [s_k])$ of $E/F$. Then all local sections of $E/F$ near $x_0$ are of the form $$ a^{r+1}[s_{r+1}] + \cdots + a^k[s_k], $$ where $a^{r+1}, \dots, a^k$ are smooth scalar functions.
There is an obvious equivalence between a local frame and a local trivialization. It is straightfoward to show that the construction above defines a compatible collection of local trivializations.