The Subset Collection axiom: $$ \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longrightarrow \exists d \in c (\forall x \in a \exists y \in d (\psi(x,y,u)) \land \forall y \in d \exists x \in a (\psi(x,y,u)))] $$ is often digested by considering the equivalent (in CZF - Subset Collection) axiom of Fullness. Let $mv(B^A)$ be the class of all sets $R \subseteq A \times B$ satisfying $\forall a \in A \exists b \in B (\langle a,b \rangle \in R)$. A set $C$ is full in $mv(B^A)$ if $C \subseteq mv(B^A)$ and $$ \forall R \in mv(B^A) \exists S \in C (S \subseteq R). $$ The Fullness axiom states: For all sets $A$ and $B$ there exists a set $C$ such that $C$ is full in $mv(B^A)$. For completness the Powerset axiom states: $\forall x \exists y \forall z(z \subseteq x \longleftrightarrow z \in y$).

Now to show that the Powerset axiom implies Subset Collection (in CZF - Subset Collection) it suffices to show that the Powerset axiom implies Fullness. This proof is claimed to be obvious in many papers. I understand this may be so but I am still having some trouble with it. The difficulty I am having is deciding which set to apply the Powerset axiom to. For $mv(B^A)$ is only assumed to be a class (although the Powerset axiom is equivalent to it being a set this result typically comes later so I don't think that is neccesary.) I must admit I am new to proving these meta-set-theoretic results so I am aware the answer is likely right under my nose. I would be delighted for someone to offer some wisdom.

The Subset Collection axiom: $$ \forall a \forall b \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longrightarrow \exists d \in c (\forall x \in a \exists y \in d (\psi(x,y,u)) \land \forall y \in d \exists x \in a (\psi(x,y,u)))] $$ is often digested by considering the equivalent (in CZF - Subset Collection) axiom of Fullness. Let $mv(B^A)$ be the class of all sets $R \subseteq A \times B$ satisfying $\forall a \in A \exists b \in B (\langle a,b \rangle \in R)$. A set $C$ is full in $mv(B^A)$ if $C \subseteq mv(B^A)$ and $$ \forall R \in mv(B^A) \exists S \in C (S \subseteq R). $$ The Fullness axiom states: For all sets $A$ and $B$ there exists a set $C$ such that $C$ is full in $mv(B^A)$. For completness the Powerset axiom states: $\forall x \exists y \forall z(z \subseteq x \longleftrightarrow z \in y$).

Now to show that the Powerset axiom implies Subset Collection (in CZF - Subset Collection) it suffices to show that the Powerset axiom implies Fullness. This proof is claimed to be obvious in many papers. I understand this may be so but I am still having some trouble with it. The difficulty I am having is deciding which set to apply the Powerset axiom to. For $mv(B^A)$ is only assumed to be a class (although the Powerset axiom is equivalent to it being a set this result typically comes later so I don't think that is neccesary.) I must admit I am new to proving these meta-set-theoretic results so I am aware the answer is likely right under my nose. I would be delighted for someone to offer some wisdom.