The axiom of extensionality states that two sets are equal if and only if they have exactly the same members: ∀A ∀B (∀x (x ∈ A ↔ x ∈ B) → A = B). This axiom eliminates any notion of internal structure, ordering, or multiplicity — a set is determined entirely by its elements, nothing more. It is the identity criterion for sets and is presupposed by virtually every proof that two sets are equal: show mutual containment. Without extensionality, {1, 2} and {2, 1} could in principle be different objects; the axiom guarantees they are one and the same set.
Practice proving set equalities by double inclusion (A ⊆ B and B ⊆ A). Then consider what mathematics would look like without extensionality — multisets and sequences are structures that intentionally violate it, which clarifies what the axiom rules out. Compare sets with other collection-like objects (bags, lists, types) to see that extensionality is a genuine choice, not a tautology.
From your overview of ZFC, you know that set theory is built on a single primitive relation: membership (∈). Everything in ZFC — numbers, functions, ordered pairs, sequences — is ultimately defined in terms of which things belong to which sets. The Axiom of Extensionality is the rule that says what it means for two sets to be *the same set*: ∀A ∀B (∀x (x ∈ A ↔ x ∈ B) → A = B). Two sets are equal if and only if they have exactly the same members. Equivalently, a set is determined entirely by its members — nothing else about it matters.
This is a genuine substantive claim, not a definition or tautology. Consider the following objects in everyday mathematics: the set {1, 2, 3}, the sequence (1, 2, 3), the multiset ⟨1, 1, 2⟩, and the tuple (1, 2, 3). All of them "contain" the numbers 1, 2, 3 in some sense, but they are different kinds of objects because they encode additional structure — order and multiplicity. The axiom of extensionality asserts that *sets* carry none of this additional structure: {1, 2, 3} and {3, 1, 2} and {1, 2, 3, 2} (if we could write that) are all the same set, because they have exactly the same members. The axiom rules out any notion of "internal arrangement" or "how many times something appears" — membership is binary, and that is all.
The practical consequence is the double-inclusion proof technique. To prove A = B, show that every element of A is an element of B (A ⊆ B) and every element of B is an element of A (B ⊆ A). Extensionality guarantees that this is sufficient: if the membership conditions agree for all x, then the sets are equal. This pattern appears constantly in mathematical proofs — whenever you need to prove two sets are equal, you unfold their definitions and verify the same elements qualify on both sides. Without extensionality, this argument wouldn't work: you could have two distinct sets with identical members, like two different empty sets.
The axiom also resolves the question of the empty set: there is exactly one set with no members. If ∅₁ and ∅₂ were two empty sets, then vacuously every member of ∅₁ is a member of ∅₂ and vice versa (there are none to check), so extensionality gives ∅₁ = ∅₂. Extensionality thus guarantees that the empty set is unique — you don't need a separate axiom asserting uniqueness. This is characteristic of how extensionality works throughout ZFC: it collapses all set-theoretic constructions to a canonical form determined solely by membership, which is what lets ZFC serve as a foundation for mathematics where "same mathematical object" has an unambiguous meaning.