Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)