Description: 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.)