A weaker version of [ax-13] with distinct variable restrictions on pairs x , z and y , z. In order to show (with ax13) that this weakening is still adequate, this should be the only theorem referencing [ax-13] directly.

Had we additionally required \( x \) and \( y' \) be distinct, too, this theorem would have been a direct consequence of [ax-5]. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. Preferably, use the version ax13w to avoid the propagation of [ax-13]. (Contributed by NM, 30-Jun-2016.) (New usage is discouraged.)