Description: Theorem showing that ax-6 follows from the weaker version ax6v .
(Even though this theorem depends on ax-6 , all references of ax-6 are
made via ax6v . An earlier version stated ax6v as a separate axiom,
but having two axioms caused some confusion.)

This theorem should be referenced in place of ax-6 so that all proofs
can be traced back to ax6v . Usage of this theorem is discouraged
because it depends on ax-13 . When possible, use the weaker ax6v rather than ax6 since the ax6v 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)(New usage is discouraged.)