Description: Deduction version of nfrexg . Usage of this theorem is discouraged
because it depends on ax-13 . See nfrexd for a version with a
disjoint variable condition, but not requiring ax-13 . (Contributed by Mario Carneiro, 14-Oct-2016)(New usage is discouraged.)