Validity of conditional CDF proof via PDF integral 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?
 A: @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).
