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 GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 25-Sep-2024.)