**Description: **A weaker version of ax-13 2382 with distinct variable restrictions on pairs
𝑥,
𝑧 and 𝑦, 𝑧. In order to show (with
ax13 2385) that this
weakening is still adequate, this should be the only theorem referencing
ax-13 2382 directly.
Had we additionally required 𝑥 and 𝑦 be distinct, too, this
theorem would have been a direct consequence of ax-5 1911.
So essentially
this theorem states, that a distinct variable condition can be replaced
with an inequality between set variables. Preferably, use the version
ax13w 2138 to avoid the propagation of ax-13 2382. (Contributed by NM,
30-Jun-2016.) (New usage is discouraged.) |