should iset.mm have both ax-bndl and ax-i12 ?

[jkingdon]

From Gérard Lang:

Considering the list of iset.mm’s axioms, it seems that ax-i12 can be proved from ax-bndl using ax-4.
The only difference between ax-bndl and ax-i12 is the third part, where ax-bndl has one more universal quantification with x. But ax-4 shows that this quantification can be suppressed.

So, as this is already taken care of with the theorem axi12, why is ax-i12 still given in the list of axioms of set.mm ?

[jkingdon]

I don't have much of an opinion about what we do here. There's been some work (at least in set.mm) to figure out where we can avoid any axiom of this sort, but I haven't done any serious looking at iset.mm in terms of where we just need ax-i12 and where we need the stronger ax-bndl.

I would defer to @benjub or anyone else who might have opinions or time to look into this matter.

[benjub]

I think that we should keep both for now. You proved that ax-bndl implies ax-i12 (over more basic axioms), and also that its full strength is not needed for much of the ensuing developments, but that it is sometimes needed. Since not all implications are clear to us, we should keep both.

As for the statements themselves, that of ax-bndl is closer to being a sentence, that is, of having no free variables (because of things like https://us.metamath.org/mpeuni/bj-dvv.html), so if a choice had to be made, I would prefer it over ax-i12.