Why does $a{\iff}b$ mean that $a$ is the definition of $b$? As an example of what I'm talking about, the axiom of extension $({\forall}A{\forall}B{\forall}x)(x{\in}A{\iff}x{\in}
B){\iff}A=B$ is often used as the definition of set equality.
Why is defining $a$ as being the same as $b$ using $a{\iff}b$ justified?
My doubts stem from things like in the following example:

Let $a$ and $b$ be WFFs.
$a{\iff}b$ means the same as "$a{\implies}b$ and $b{\implies}a$"
$a{\implies}b$ is defined as ${\lnot}(a{\land}{\lnot}b)$
Let $c$ be $x{\land}y$.
Let $d$ be $x{\lor}y$.
Let both $c$ and $d$ be true.
By the above definition of $a{\implies}b$ it's always true that $c{\implies}d$.
Since $c$ is true and $d$ is true, it's also true that ${\lnot}(d{\land}{\lnot}c)$. Therefore $d{\implies}c$
Therefore $c{\iff}d$

However, we know that $x{\land}y$ and $x{\lor}y$ are different things, so it's not true that $c{\iff}d$.
 A: "$a\iff b$" does not in itself mean that it is a definition.
However, it can be used to express a definition, if we explicitly say that what we're doing is defining $b$ (or $a$). In that case, once we're using that definiton $a\iff b$ will always be true because it's been declared to be the definition.
Note, though, that you can't just pick to random wffs and define them to mean the same. In the particular case of your extensionality axiom however, one of the formulas was $A=B$, which is a previously undefined predicate applied to different variable letters. In that particular case, all that is needed to define a meaning for $=$ is exactly an equivalence of this kind, which will allow you rewrite any atomic formula of the form $t_1=t_2$ into one that doesn't involve the $=$ symbol.
Not all of the communicative content of mathematics is visible in the symbolic formulas. The text around them connects the formulas is also important, oftentimes more than the formulas.

In your particular example, confusion results because you're not careful about whether the reasoning you're doing is supposed to be valid under all interpretations of the variables, or just for a particular one. Here you're explicitly saying, "Let both $c$ and $d$ be true", and everything you conclude thereafter is under that assumption.
It is indeed the case that if both $x\land y$ and $x\lor y$ are true then $x\land y\iff x\lor y$ is also true. That does not imply anything about how $x\land y$ and $x\lor y$ relate to each other in worlds where they are not both true.
A: You are saying:

Let both $c$ and $d$ be true.

But this is not the only case; we have also the other cases; in particular, when $x$ is true and $y$ is false, we have that:

$x \lor y$ is true and $x \land y$ is false.

Thus: 


$x \lor y \Rightarrow x \land y$, i.e. $d \Rightarrow c$ is false. 



Regarding Extensionality we have two possibilities; either:
(i) develop set theory using first-order language with equality; in this case the equality is "already there" in the language, and the axiom will be:

$∀x∀y \ [∀z(z \in x ↔ z \in y) → x=y]$;

or
(ii) develop the theory in a language without equality, and introduce the equality with a definition:

$∀x∀y \ [x=y ↔ ∀z(z \in x ↔ z \in y)]$.

