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)$ I managed to prove existence for the following theorem: 
$$\forall A\in\mathcal{P}(U)\ \exists!B\in\mathcal{P}(U)\ \forall C\in\mathcal{P}(U)\ (C\setminus A=C\cap B)$$
where U is any set. My assumption is that $B=U\setminus A$, and it works for existence, but I'm stuck with proving uniqueness part with $B$ being defined this way.
For uniqueness we need to prove
$$\forall B'\in\mathcal{P}(U)\ \forall C\in\mathcal{P}(U)\ (\ (C\setminus A=C\cap B')\rightarrow B'=B)$$
where A is arbitrary element of $\mathcal{P}(U)$ but I don't how to connect $x\in B'$ or $x\in B$ to the assusmed identitiy $C\setminus A=C\cap B'$.
Any pointers are much appreciated.
EDIT
Here is my attempt of proof.
Proof: Let $A$ be an arbitrary element of $\mathcal{P}(U)$ and let $B=U\setminus A$.
Existence: Let $C$ be an arbitrary element of $\mathcal{P}(U)$. $(\rightarrow)$ Let $x$ be an arbitrary element of $C\setminus A$. Since $C\subseteq U$, then $x\in U\setminus A$. Therefore $x\in C\cap B$. $(\leftarrow)$ Let x be an arbitrary element of $C\cap B$. Then $x\in C\cap (U\setminus A)$, so we can conclude $x\in C\setminus A$.
Uniqueness: Let $B'$ be an arbitrary element of $\mathcal{P}(U)$ and suppose $\forall C\in\mathcal{P}(U)(C\setminus A=C\cap B')$.
$(B'\subseteq B)$ Since $B'\in\mathcal{P}(U)$, then in particular $B'\setminus A=B'\cap B'=B'$, so clearly $B'\cap A=B'\cap (U\setminus B)=\varnothing$. Then $\forall x(x\not\in B'\lor x\not\in U\lor x\in B)$, which is equivalent to $\forall x(x\in B'\cap U\rightarrow x\in B$). Since $B'\subseteq U$, $B'\cap U=B'$, we now have $\forall x(x\in B'\rightarrow x\in B)$, and therefore $B'\subseteq B$.
$(B\subseteq B')$ Let $C=B$. Then $B\setminus A=B\cap B'$, and because $B\cap A=\varnothing$, we have $B=B\cap B'$, so we can conclude $B\subseteq B'$.  
 A: 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’).
A: 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...
A: Hint: Plug $B$ into the $C$ from the $B'$ assertion to get that $B\setminus A\subseteq B'$, and similarly for $B'$ into $C$ from the $B$ assertion, to have $B'\setminus A\subseteq B$.
Now show that $B'\setminus A=B'$ and $B\setminus A=B$ (plug $C=\varnothing$ into both assertions) and you are done.
A: Let $B := U \setminus A$. 
Let $B' \subseteq U$ be any subset that satisfies the hypothesis: $\forall C \in \mathcal P(U) (C \setminus A = C \cap B')$
Case I:  
Assume $x \in B' \setminus B$.
\begin{align*}
  \implies & x \in A \\
  \text{Let } & C = \{x\} \\
  \implies & \left( C \setminus A \right) = \varnothing \ne C = \left( C \cap B' \right) \\
  \implies & \impliedby (contradiction)
\end{align*}
Case II:  
Assume $y \in B \setminus B'$.
\begin{align*}
  \implies & y \notin A \\
  \text{Let } & C = \{y\} \\
  \implies & \left( C \setminus A \right) = C \ne \varnothing = \left( C \cap B' \right) \\
  \implies & \impliedby (contradiction)
\end{align*}
$\implies B'=B$ is unique.
A: I think this even might be an easier proof:
Proof. 
Existence. Let $A$ be an arbitrary element of $\mathscr P(U)$ and let $B = U\setminus A ∈ \mathscr P(U)$. Then clearly for every $C ∈ \mathscr P(U)$, $C ∩ B = C ∩ U\setminus A = C\setminus A$.
Uniqueness. Let $A$ be an arbitrary element of $\mathscr P(U)$. To see that $B$ is unique, suppose that $B' ∈ \mathscr P(U)$ and for all $C ∈ \mathscr P(U)$, $C\setminus A = C ∩ B'$. Then in particular, taking $C = U$, we can conclude that $U\setminus A = U ∩ B' = B'$. So we have $B' = U\setminus A = B.$
