The axiom of extensionality tells us that whenever two sets have all the same members then they are equal.
The properties of equality tell us that the converse is also true.
From these two we infer that a two sets are equal *iff* they have the same members, and this is a boolean equality which can conveniently be used as a rewriting rule.

The application of this rule will prove to be more delicate than that of extensionality in the typed set theory available in HOL (in effect as a congenial syntax for talking about properties).
This is because in a typed set theory repeated application of the principle eventually translates all set equations into talk about elements, but in a pure untyped set theory, only sets exist and rewriting with the principle of extensionality may never terminate.