Dral1v

[wlammen]

Continuation of #3898
Main: replace dral1v with wl-dral1v, so it is now based on ax12v only, avoiding axc11r, as shortly discussed here #3879 (comment)

[GinoGiotto]

So by reading your suggestion, I guess you plan to convert the current axc11r to axc11rALT?

[wlammen]

I don't know whether axc11r is provable from ax-10, ax-11, ax12v and ax-13. I am pretty sure this was investigated before, most probably I was involved in it, but I don't know the outcome any more.
So without knowing anything, it is a matter of taste, whether you view axc11r (ax12v being the proper refinement of ax-12) as an exotic axiom, like currently ax-13.
See https://us.metamath.org/mpeuni/axc11.html for an estimate to what axc11r roughly amounts to, axiom-wise. axc11 is discouraged, but axc11r not, which looks odd IMO.
I am not going to push anything in that direction, but if you discourage the use of ax-13, axc11, I think it is consequent to apply the same restriction to axc11r. That way a preference of a possible combined use of ax-10, ax11, ax12v in proofs is enforced.
Whatever my contribution will be, I will set out in my mathbox first, and let others decide which path to follow.