Description: Variation on nfexd which adds the hypothesis that x and y are
distinct in the inner subproof. Usage of this theorem is discouraged
because it depends on ax-13 . Check out nfexd for a version
requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016)(New usage is discouraged.)