Description: All variables are effectively bound in a distinct variable specifier.
Version of nfnae with a disjoint variable condition, which does not
require ax-13 . (Contributed by Mario Carneiro, 11-Aug-2016) Avoid
ax-13 . (Revised by Gino Giotto, 10-Jan-2024)(Proof shortened by Wolf Lammen, 25-Sep-2024)