 Extensional relation

A relation is extensional when distinct elements have distinct sets of predecessors.

This is the predecessor-set instance of the identity principle extensionality.