In Martin-Löf's "Intuitionistic Type Theory", we can judge two sets are "equal" if the following are true:
$$ membership\ rules: \frac{a \in A}{a \in B} and \frac{a \in B}{a \in A}\\ identity\ rules: \frac{a = b \in A}{a = b \in B} and \frac{a = b \in B}{a = b \in A} $$
Are both sets of rules necessary? That is, are there cases where the membership judgments would hold but the sets wouldn't be equal (or the other way around)?
Also, how does one read $a=b \in A$? I assume the right chunking is $a = (b \in A)$, which I expect means something like $\exists b : B. a = b$. But if it is senseless to talk about something independently of that thing being a member of the set, why didn't Martin-Löf write $(a \in A) = (b \in A)$ or $\exists a b:A. a = b $. Or, since equality questions only have sense in relation to some set, why not $a =_A b$?