|Description: Rederivation of axiom ax-5 1533
from the orginal version, ax-5o 1694. See
ax5o 1693 for the derivation of ax-5o 1694 from ax-5 1533.
This theorem should not be referenced in any proof. Instead, use ax-5 1533
above so that uses of ax-5 1533 can be more easily identified.
Note: This is the same as theorem alim 1548 below. It is proved separately
here so that it won't be dependent on the axioms used for alim 1548.
(Contributed by NM, 23-May-2008.) (Proof modification is discouraged.)
(New usage is discouraged.)