Reversed substitution. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.)
Reversed substitution. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.)