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/49832dd9-c7fd-4e54-92b5-67341898c4fbn%40googlegroups.com.
