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?
On Tuesday, October 14, 2025 at 11:00:29 AM UTC-4 Matthew House wrote: > In set.mm, ax-11 <https://us.metamath.org/mpeuni/ax-11.html> 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 > <https://us.metamath.org/mpeuni/ax-13.html>? If not, it would seem like > we should create a new ax11v and have everything go through that, the same > as ax6v <https://us.metamath.org/mpeuni/ax6v.html> and ax12v > <https://us.metamath.org/mpeuni/ax12v.html>. > > Matthew House > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/e525e8e3-4d5d-45fd-8804-42d57be01f7dn%40googlegroups.com.
