Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.


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'$.

share|cite|improve this question
up vote 3 down vote accepted

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.

share|cite|improve this answer
I don't see any inference rule that would bring me from supposing $x\in B$ or $x\in B'$ to $x\in C$ or $x\not\in C$, except for proving by cases $x\in C$ and $x\not\in C$. If not going for elementhood, how exactly do I plug B or B' into C? – LavaScornedOven Dec 8 '12 at 12:57
If the claim is true for all $C$ then it is true for $C=B'$, for example, therefore $B'\setminus A=B\cap B'$. Show that $B'\setminus A=B'$ then you have that $B'=B\cap B'$; similarly $B=B\cap B'$. From this you can directly deduce the conclusion of equality. – Asaf Karagila Dec 8 '12 at 13:02
Oh, I see. (Palmface...) :) I missed the fact that I can plug into $C\setminus A=C\cap B'$ whatever I wont from $\mathcal{P}(U)$. Thanks for the help. – LavaScornedOven Dec 8 '12 at 13:18
No problem! (I think it's facepalm, by the way, not palmface :-)) – Asaf Karagila Dec 8 '12 at 13:52
Facepalm would do, but check this out: – LavaScornedOven Dec 8 '12 at 14:49

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’).

share|cite|improve this answer

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"} \\ & 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...

share|cite|improve this answer
Where could I find material with that proving "style"? It looks interesting to explore. – LavaScornedOven Mar 19 '13 at 12:13
@LavaScornedOven See the note at the end of another answer of mine./11994. – Marnix Klooster Mar 19 '13 at 13:39
Thanks for the reply. I'm currently investigating different approaches, and your suggestion comes as very helpful. – LavaScornedOven Mar 20 '13 at 2:14

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.