|Description: Derivation of set.mm's
original ax-11o 2080 from ax-10 2079 and the shorter
ax-11 1715 that has replaced it.
An open problem is whether this theorem can be proved without relying on
ax-16 2083 or ax-17 1603 (given all of the original and new
versions of sp 1716
through ax-15 2082).
Another open problem is whether this theorem can be proved without
relying on ax12o 1875.
Theorem ax11 2094 shows the reverse derivation of ax-11 1715 from ax-11o 2080.
Normally, ax11o 1934 should be used rather than ax-11o 2080, except by
theorems specifically studying the latter's properties. (Contributed by