Description: Version of df-nfc with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019)