Given the question: $$\text{Show that}\ F_X(x\mid A) = \dfrac{\Pr(A\mid X\leq x)}{\Pr(A)}\cdot F_X(x)$$
I have seen the solution via probabilities 'directly'.
My question is whether the following method was (unnecessary extra work, but nonetheless) valid:
\begin{align} & F_X(x\mid A) = \int_{-\infty}^x f_X(t\mid A)\, dt \\[8pt] = {} & \int_{-\infty}^x \dfrac{\Pr(A\mid X=t)}{\Pr(A)} f_X(t)\, dt \\[8pt] = {} & \dfrac{\Pr(A\mid X\leq x)}{\Pr(A)} \int_{-\infty}^x f_X(t)\, dt \\[8pt] = {} & \dfrac{\Pr(A\mid X\leq x)}{\Pr(A)}\cdot F_X(x) \end{align}
I suppose my doubts lie in the original formulation as integral of $f_X(x\mid A)$, and also the extraction of $\Pr(X=x)$ to be $\Pr(X\leq x)$ outside the integral - which seems to intuitively make sense, but I'm not sure that's actually sound?
@Michael Hardy, you are definitely correct. Also, I found this question interesting since it kind of connects the undergraduate notions of conditional probability with the measure theoretical definitions. This is too long for a comment so I just posted it as an answer. See if I got this correct:
Given a probability space $(\Omega,~\mathcal{F},P)$, define the sub-$\sigma$ algebra of $\mathcal{F}$ as
$$ \mathcal{G}=\{\emptyset,~A,~A^c,~\Omega\}, $$ for some set $A\in\mathcal{F}$. Then, we have $E[1_B~|~\mathcal{G}]$ satisfies $$ E[1_B~|~\mathcal{G}]\int_Af_X(t)dt =\int_A1_B(t)f_X(t)dt,~\textrm{on}~A,~~~~(1) $$ where $1_B(\cdot)$ is the indicator function. We didn't take quotient for the reason which is commented by @Michael Hardy above. This can be readily verified by computing
$$ E[E[1_B~|~\mathcal{G}];~A]=\int_AE[1_B~|~\mathcal{G}]f_X(t)dt =\int_A1_B(t)f_X(t)dt=E[1_B;~A]. $$ For simplicity, we will denote $E[1_B~|~\mathcal{G}]$ on $A$ as $E[1_B~|~A]$.
Similarly, it can be verified that $E[1_A~|~X\leq x]$ satisfies
$$ E[1_A~|~X\leq x]\int_{-\infty}^xf_X(t)dt =\int_{-\infty}^x 1_A(t)f_X(t)dt.~~~~(2) $$
With these preparations, I can work out a similar proof as OP but in a more strict way: \begin{align} F_X(x~|~A)=&E[1_{\{X\leq x\}}~|~A]\\ =&\frac{\int_A1_{\{X\leq x\}}(t)f_X(t)dt}{\int_Af_X(t)dt}\\ =&\frac{\int_{-\infty}^x1_{A}(t)f_X(t)dt}{\int_Af_X(t)dt}\\ =&\frac{E[1_A~|~X\leq x]\int_{-\infty}^xf_X(t)dt}{\int_Af_X(t)dt}\\ =&\frac{Pr(A~|~X\leq x)F_X(x)}{Pr(A)}, \end{align}
where the second equality follows from $Pr(A)>0$ and (1), and the fourth equality follows from (2).