Proof of Restricting a σ-Algebra or a Measure Twice

Throughout, for classes $\mathcal{G}$ and $S$ and a set $C$, $C\in\mathcal{G}_{S}$ holds if and only if $C\in\mathcal{G}$ and $C\subseteq S$, by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii).

Proof of (i). Let $A\subseteq X$ and let $C$ be a set. Then $C\in(\mathcal{F}_{X})_{A}$ if and only if $C\in\mathcal{F}$, $C\subseteq X$ and $C\subseteq A$, while $C\in\mathcal{F}_{A}$ if and only if $C\in\mathcal{F}$ and $C\subseteq A$. Since $C\subseteq A$ and $A\subseteq X$ give $C\subseteq X$ ($\subseteq$ is transitive, by Subclasses and Subsets (i)), the two conditions are equivalent. Hence $(\mathcal{F}_{X})_{A}=\mathcal{F}_{A}$ by Axiom of Extensionality for Classes.

Proof of (ii). Let $B\subseteq A$. By (i), applied with $A$ in place of $X$ and $B$ in place of $A$,

$$(\mathcal{F}_{A})_{B}=\mathcal{F}_{B}.$$

Moreover $\mathcal{F}_{B}\subseteq\mathcal{F}_{A}$: an element $C$ of $\mathcal{F}_{B}$ satisfies $C\in\mathcal{F}$ and $C\subseteq B$, hence $C\subseteq A$ ($\subseteq$ is transitive, by Subclasses and Subsets (i)), so $C\in\mathcal{F}_{A}$. Therefore, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iv) with $H=\mu$, $S=\mathcal{F}_{A}$ and $T=\mathcal{F}_{B}$,

$$(\mu_{A})|_{(\mathcal{F}_{A})_{B}}=(\mu|_{\mathcal{F}_{A}})|_{\mathcal{F}_{B}}=\mu|_{\mathcal{F}_{B}}=\mu_{B}.$$