Formal basis for computing the differential in trig substitution To compute the following integral
$$\int_{-1}^{1} \sqrt{1-x^2} \, dx$$
we use trig substitution and introduce the change of variable $x := \sin(\theta)$ where
$$-\frac{\pi}{2} \leq \theta \leq \frac{\pi}{2}$$
To compute the differential $dx$ with respect to $\theta$, we let
$$\frac{dx}{d\theta} = \cos(\theta) \iff dx = \cos(\theta) \, d\theta$$
and we eventually have
$$\int_{-\frac{\pi}{2}}^{\frac{\pi}{2}} \sqrt{1-\sin(\theta)^2} \cos(\theta) \, d\theta$$
However, to get $dx$ with respect to $\theta$, we cancel out the differentials by separating them in the last step which does not seem very formal from a mathematical standpoint. What is the formal basis behind the substitution of $dx$ by $\cos(\theta) \, d\theta$ apart from this algebraic manipulation?

Got it. Trig substitution is $u$-sub applied backwards where $x$ is a function of $\theta$ so that
$$\int_{a}^{b} f(\varphi(\theta))\varphi'(\theta) \, d\theta = \int_{\varphi(a)}^{\varphi(b)} f(x) \, dx$$
where $x := \varphi(\theta)$ so by identification we also have $dx := \varphi'(\theta) \, d\theta$. Granted that $\varphi$ is continuous and differentiable on the bounds of integration.
Applying the same reasoning to the following integral
$$\int_{-1}^{1} \sqrt{1 - x^2} \, dx$$
we eventually obtain
$$\int_{-\frac{\pi}{2}}^{\frac{\pi}{2}} \sqrt{1 - \sin(\theta)^2} \cos(\theta) \, d\theta = \int_{\sin\left(-\frac{\pi}{2}\right)}^{\sin\left(\frac{\pi}{2}\right)} \sqrt{1 - x^2} \, dx$$
where $x := \sin(\theta)$ and $dx := \cos(\theta) \, d\theta$.
This method is justified by the fact that $\sin(\theta)$ when
$$-\frac{\pi}{2} \leqslant \theta \leqslant \frac{\pi}{2}$$
is continuous and differentiable.
