Description: Bound-variable hypothesis builder for disjoint collection. Version of
nfdisj with a disjoint variable condition, which does not require
ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) Avoid
ax-13 . (Revised by Gino Giotto, 26-Jan-2024)