It is known that ax-10, ax-11, and ax-12 are logically redundant in a weak sense. Practically, they can be replaced with hbn1w, alcomimw, and ax12wlem as long as you can fully substitute for in the relevant wff (that is, cannot appear in the wff after substituting).
This strategy (which I will call a "standard replacement" of axioms) has a lot of potential, for example it works with df-fv and df-mpt, two very common constructions. But doing a standard replacement of ax-10, ax-11, and ax-12 takes unsatisfyingly long. Usually, if another approach is found, that approach is shorter and better.