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