Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker sb6rfv if possible. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.)