|Description: Derivation of set.mm's
original ax-11o 2177 from ax-10 2176 and the shorter
ax-11 1753 that has replaced it.
An open problem is whether this theorem can be proved without relying on
ax-16 2180 or ax-17 1623 (given all of the original and new
versions of sp 1755
through ax-15 2179).
Another open problem is whether this theorem can be proved without
relying on ax12o 1969.
Theorem ax11 2191 shows the reverse derivation of ax-11 1753 from ax-11o 2177.
Normally, ax11o 2033 should be used rather than ax-11o 2177, except by
theorems specifically studying the latter's properties. (Contributed by