Unique Existence In Local Set Theories I am working through Toposes and Local Set Theories by Bell. I would like to know the proof of this expression from page 82:
$$(\exists ! w)\alpha, \alpha(w/true),\alpha \vdash w = true $$
I would like the proof to be based on local set theory/ Mitchell–Bénabou language (i.e., the internal language of a topos).
Any help would be much appreciated.
 A: This may be a bit tedious so let me give you an outline (references are from Bell):

*

*Expand the definition of $\exists!$
$$\exists w.(\alpha\wedge \forall u.\alpha(w/u)\to w=u),\alpha(w/true),\alpha\vdash w=true$$


*Use proposition 3.7.3 to eliminate the existential on the left and introduce a fresh variable $v$,
$$\alpha(w/v)\wedge\forall u.\alpha(w/u)\to v=u,\alpha(w/true),\alpha\vdash w=true$$


*Use proposition 3.3.1 to eliminate the conjunction on the left
$$\alpha(w/v),\forall u.\alpha(w/u)\to v=u,\alpha(w/true),\alpha\vdash w=true$$


*Use proposition 3.4.7 to eliminate the universal on the left and substitute $u/true$
$$\alpha(w/v),\alpha(w/true)\to v=true,\alpha(w/true),\alpha\vdash w=true$$


*But we can also use 3.4.7 to eliminate the universal on the left and substitute $u/w$
$$\alpha(w/v),\alpha(w/w)\to v=w,\alpha(w/true),\alpha\vdash w=true$$


*Putting these together, (noticing that we don't even need $\alpha(w/v)$, and also that $\alpha(w/w) = \alpha$), we obtain
$$\alpha\to v = w, \alpha(w/true)\to v = true,\alpha(w/true),\alpha\vdash w = true$$
The result then follows by applying transitivity (and a few applications of modus ponens/cut).
