Why use the biconditional in the Axiom of Extensionality I'm studying the Axiom of Extensionality in the following form:
$$
\forall a \forall b[\forall x(x\in a\leftrightarrow x\in b)\rightarrow a=b]
$$
(where quantification of a,b is restricted to sets and quantification of x can range over domain objects as well as sets)
What is the advantage of the preceding formulation over the following, where the biconditional is replaced with conjunction? E.g.
$$
\forall a \forall b[\forall x(x\in a\wedge x\in b)\rightarrow a=b]
$$
I am aware that conjunction and the biconditional are not logically equivalent since their truth tables differ in the case where both argument propositions are false.
So it seems that these two forms should differ in the case where an element of the domain is neither in a nor b.
Using the conjunction form, this case makes the main conditional of the axiom  vacuously true ($False\rightarrow True$). Using the biconditional form, this case makes the main conditional of the form $True\rightarrow True$. Either way, the main conditional is true.
So, what is the advantage of the biconditional form?
 A: $\forall x(x\in a\land x\in b)$ is always false, so your version is vacuously true of all sets $a$ and $b$.
A: Recall that the inference rule for implication states that if we know $\phi$ is true, and if we know that $\phi\rightarrow\psi$ is true, then we can deduce that $\psi$ is true. Notice that it does not also say that if we know $\phi$ is false, and $\phi\rightarrow\psi$ is true, that we can deduce $\psi$ is true. Indeed, it better not because then (because of LEM) whenever $\phi\rightarrow\psi$ is true, $\psi$ would be true, which is absurd).
Now, there is a slight with your analysis of the two axioms, a small circularity: you consider only how the axioms instantiates when you already have $a=b$, and you do case analysis on whether there is an $x$ in $a$ or not. You need to also consider the case when $a\neq b$. This error doesn't make a difference though, it only obscures what happens because you should consider if $x\in a$ or not independently of whether $a=b$.
You see, we want the axiom to allow us to conclude $a=b$ under appropriate conditions. With the biconditional form, it is clear that we can derive $a=b$ if we have a way of showing that for every $x$, $x\in a\rightarrow x\in b$ and $x\in b\rightarrow x\in a$, which is exactly what we want.
With the conjunction form, we can derive $a=b$ if for every $x$, $x\in a$ and $x\in b$. In particular, we can only derive $a=b$ if $a$ and $b$ both contained every possible $x$. If there were an $x\not\in a$ (or an $x\not\in b$), then the axiom becomes False${}\rightarrow a=b$, so we cannot derive $a=b$. To think what would happen to Set theory when this is the case, imagine that you have different colored sets that have the same elements (unless they contain everything, which i think Russel's paradox might still go through so such sets don't exist). Then applying comprehension to craft an empty set, will give you many differently colored empty sets, which you wouldn't be able to prove are equal.
A: Elaborating slightly on Brian's answer: although both versions of extensionality are true, in formulating axioms for set theory (or for any other theory) we don't merely want true axioms. Compare your thought with the following:
Consider:
(*) If you put your hand in a fire, it will get burned 
Putting strange exceptions to one side, (*) is true. But so, vacuously, is:
(**) If you put your hand in a fire, you put your hand in a fire
So why use (* ) and not merely (**)? 
A: "There are two distinct empty sets" is a sentence that is independent of $E'+C$, where $C$ denotes Comprehension and $E'$ denotes the variant of Extensionality proposed above. In contrast, that sentence is false in $E+C$, where $E$ denotes Extensionality.
One way to contrast $E'$ to $E$ is to read them in the contrapositive: if $a \neq b$, then $E$ requires an element in the symmetric difference of $a$ and $b$, whereas $E'$ is satisfied merely by an element outside of the union of $a$ and $b$. (In case $a$ and $b$ have no elements, then $E'$ is satisfied merely by letting $a \neq b$.)
