Description: Theorem showing that ax-6 1964
follows from the weaker version ax6v 1965.
(Even though this theorem depends on ax-6 1964,
all references of ax-6 1964 are
made via ax6v 1965. An earlier version stated ax6v 1965
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 1964
so that all proofs
can be traced back to ax6v 1965. When possible, use the weaker ax6v 1965
rather than ax6 2386 since the ax6v 1965
derivation is much shorter and requires
fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM,
25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) Usage of
this theorem is discouraged because it depends on ax-13 2374. Use ax6v 1965
instead. (New usage is discouraged.) |