Uniqueness proof for $\forall A\in\mathcal{P}(U)\ \exists!B\in\mathcal{P}(U)\ \forall C\in\mathcal{P}(U)\ (C\setminus A=C\cap B)$

HINT: An easier way is to show that if $B\ne U\setminus A$, there is a $C\in\wp(U)$ such that $C\setminus A\ne C\cap B$. You’ll want to consider two cases, $B\cap A\ne\varnothing$ (loosely, ‘$B$ is too big’) and $A\cup B\ne U$ (loosely, ‘$B$ is too small’).

Here is my attempt at a direct proof for this theorem. Note that $A$, $B$, etc. denote subsets of our 'universe' $U$, and $x$ denotes an element of U.

We start out by simplifying everything inside $\exists!$, as follows: $$ \begin{align*} & \langle \forall C :: C \setminus A \;=\; C \cap B \rangle \\ \equiv & \;\;\;\;\;\text{"extensionality; definitions of $\setminus$ and $\cap$"} \\ & \langle \forall C :: \langle \forall x :: x \in C \land x \notin A \;\equiv\; x \in C \land x \in B \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: move $x \in C$ out of $\equiv$, then into range"} \\ & \langle \forall C :: \langle \forall x : x \in C : x \not\in A \equiv x \in B \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: what Dijkstra calls shunting"} \\ & \langle \forall x : \langle \exists C :: x \in C \rangle : x \not\in A \equiv x \in B \rangle \\ \equiv & \;\;\;\;\;\text{"range is true: take $C:=\lbrace x \rbrace$"} \\ & \langle \forall x :: x \not\in A \equiv x \in B \rangle \\ \equiv & \;\;\;\;\;\text{"definition of complement; extensionality"} \\ & B = A^c \\ \end{align*} $$ This trivially proves existence and uniqueness, but for completeness I will spell it out anyway. Using the following not-so-well-known definition of $\exists!$ (where $w$ is a fresh variable) $$ \langle \exists! v :: P \rangle \;\equiv\; \langle \exists w :: \langle \forall v :: P \:\equiv\: v=w \rangle \rangle $$ the original theorem is proven as follows: $$ \begin{align*} & \langle \forall A :: \langle \exists! B :: \langle \forall C :: C \setminus A \;=\; C \cap B \rangle \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"by the above calculation"} \\ & \langle \forall A :: \langle \exists! B :: B = A^c \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"by the above definition"} \\ & \langle \forall A :: \langle \exists B' :: \langle \forall B :: B = A^c \:\equiv\: B = B' \rangle \rangle \rangle \\ \Leftarrow & \;\;\;\;\;\text{"what Dijkstra calls Leibniz' rule"} \\ & \langle \forall A :: \langle \exists B' :: A^c = B' \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: what Dijkstra calls the one-point rule"} \\ & \langle \forall A :: \mathrm{true} \rangle \\ \equiv & \;\;\;\;\;\text{"logic"} \\ & \mathrm{true} \\ \end{align*} $$

Hope this helps...