I recently saw the Kuratowski Formalization of an ordered pair, and decided to take a crack at proving it does what it says. I tried to consider the 3 cases of $(a,b)=(c,d)$, either $a=b=c=d$, $a=b, c \neq d$ (without loss of generality), and $a\neq b, c \neq d$.
Some things I'm concerned about:
In the $\implies $ direction, I assume $(a,b)=(c,d)$ and then in case 1 I also assume $a=b,c\neq d$. This leads to a contradiction to one of my assumptions (I think to $(a,b)=(c,d)$) but I don't know how to tell for sure. (Contradicting the first assumption $(a,b)=(c,d)$ would be best since it would prove the theorem vacuously in this case.)
Any other comments or tips would be appreciated, I'm a bit rusty.
edit: The last sentence of the proof should read: Therefore $d=b$.
Here is another way to prove it: if $(a,b)=(c,d)$, then intersection $\bigcap(a,b) = \{a\}\cap \{a,b\}$ of $(a,b)$ and the intersection of $(c,d)$ are same. Therefore we have $\{a\}=\{c\}$ and we have $a=c$.
Now consider the union $\bigcup(a,b) = \{a,b\}$, so we have $\{a,b\}=\{c,d\}$. If $a=b$, then $\{a\}=\{a,d\}$ so $a=d$. Otherwise, so if $a\neq b$, then we can take difference by $\{a\}$ in both sides of the equality and we get $\{b\}=\{d\}$.