Replacing Axiom of Extensionality with a logical formalism Is it possible to replace the Axiom of Extensionality with a formalism from logic, namely the following one: $\forall a \forall b (a=b\Leftrightarrow \forall P (P (a)\Leftrightarrow P (b)))$ ($ P $ is obviously a predicate)?
 A: In general, the axiom
$$
(\forall P)[P(a) \Leftrightarrow P(b)] \Rightarrow a=b
$$
is an extensionality axiom. It goes by the name "Leibniz' law".
The first problem, though, it how to quantify over $P$. Usually this is done in second-order logic, rather than first-order logic. 
In first-order logic, the kind used to study ZFC, the only quantification possible is over sets. One cannot quantify over formulas, predicates, or anything else. Without the axiom of extensionality, it is possible that two sets could contain all the same elements, but still be nonequal. This could happen, for example, if each set also has a "label" which is visible to us but not visible to the language of ZFC. For a real-life analogy, a math class and history class could contain the same students without being the same class. 
In second-order logic, if we take the quantifier over predicates to range over all predicates, then as the answer by Hagen von Eitzen indicates we can consider the predicate $P_a(x) \equiv x = a$. However, as explained at Wikipedia, philosophers studying Leibniz' law may reject the predicate $P_a$ because it makes the law trivial. There is also an article on Leibniz' law at the Stanford Encyclopedia of Philosophy.
A: As Peter remarked, the axiom you have defined is not a first-order axiom because you quantify over predicates. 
One way to solve this is that instead of quantifying over predicates, you add a schema over all the predicates in the language. But the language of set theory only contains one extralogical symbol: $\in$, and that's a binary relation.
One way to solve that is to add an axiom schema over all formulas with exactly one free variable. But that's not a good result, because in some models of set theory you can find indiscernible elements which satisfy, amongst other things, the same formulas with one free variable.
But the axiom of extensionality has a different role. It has the role of allowing models of set theory to distinguish their objects internally only by using $\in$. In fact, in some very old texts where $=$ was not often included in the language (or the logic), the symbol $=$ was defined in a way which rendered the axiom of extensionality vacuously true.
A: The $\Rightarrow$ part of what you wrote is already part of the equality axioms assumed in first order logic (though it's really an axiom scheme if we want to stay within first order logic).
For the other direction, assuming $a\ne b$ the predicate $P(x)\equiv x=a$ is one with $P(a)\not\Leftrightarrow P(b)$, hence nothing is gained.
The axiom of extensionality is more than this: It states that different sets can be distinguished by the elements they contain. There are no two sets with the same elements but different haircolour.
A: Your definition of identity, where you quantify into predicate position, is indeed  standardly available in second-order logic. But moving from first-order ZF(C) to a second-order formulation in general -- where e.g. you can now trade in all the instances of the separation axiom-schema for a single second-order axiom -- makes for a significant strengthening of the theory, which is not what you intended I imagine.
