Can ax-11 be rederived from its DV form without ax-13?

[Matthew House]

In set.mm, ax-11 is written as |- ( A. x A. y ph -> A. y A. x ph ), with no DV restrictions between x and y. Can it be derived as a theorem from the weaker form with the additional restriction $d x y, without using ax-13? If not, it would seem like we should create a new ax11v and have everything go through that, the same as ax6v and ax12v.

Matthew House

[Matthew House]

Actually, I'm not even sure if the ax11v → ax-11 rederivation can be performed with access to ax-13. The usual approach with distinctors runs into |- ( -. A. y y = x -> F/ y A. x A. y ph ), which isn't trivial with ax11v. The obvious idea would be to use a proper substitution to change the variable and then apply ax11v, but the proper substitution itself would require the full ax-11 to move through the quantifier. Perhaps there's a more clever kind of substitution that would work?