ZF Axiom of Extensionality implies unique determination? The Principle/Axiom of Extensionality says sets that have the same elements are equal, i.e.,
$$\forall x (x \in A \iff x \in B) \implies A = B$$
But I've seen in texts the statement that the AoE implies that a set $S$ is uniquely determined by its elements

The axiom expresses the basic idea of a set: A set is determined by
its elements.

I suppose some sort of proof would enlighten me, but to declare a set as a collection of elements seems fairly basic, nothing further needed. So why is an axiom about equality of sets bolstering the basic idea of a set being determined by its elements?
 A: Saying a set is uniquely determined by its elements is really just an informal rephrasing of the AoE. So your right, its not really something you would prove. First, because it is phrased to imprecisely to be given a rigorous proof. Second, if you took the time to formulate it precisely, you would just end up with the axiom of extensionality (or something equivalent to it).
Now, to answer why the AoE is necessary. As you mention, if we already know that the objects we are working with are sets, then extensionality should just be true, no axiom necessary. But, the problem is that, when setting up the axioms of ZF, we do not already know that we are working with sets. Something a bit different is going on.
Essentially, in ZF, "set" and "$\in$" are undefined terms. They do not have a definition, like you might find a definition of "set" or "collection" in ordinary language. Rather, in ZF, "set" and "$\in$" are taken as primitive things. So we do not know that we are working with sets (as from ordinary language), even though we call these things "sets". Rather, what happens is that we impose axioms that every objects in (a model of) ZF must satisfy. The hope is that by imposing the right axioms, we can get these primitive undefined objects (what we call "sets" in ZF) and primitive undefined relation "$\in$" (what we call "membership" in ZF) to behave like the corresponding intuitive and pre-theoretical concept of set and membership from ordinary language. This is in fact why we call the concepts from ZF "set" and "membership". So the reason we have to assert the AoE is to get the undefined notion of "set" is ZF to behave like an actual set. We would not be able to "prove" the AoE since the objects of ZF really are just primitive and undefined things. But they are forced to behave like sets through the axioms.
