Description: One direction of a simplified definition of substitution. The converse
requires either a disjoint variable condition ( sb5 ) or a nonfreeness
hypothesis ( sb5f ). Usage of this theorem is discouraged because it
depends on ax-13 . Use the weaker sb1v when possible. (Contributed by NM, 13-May-1993) Revise df-sb . (Revised by Wolf Lammen, 21-Feb-2024)(New usage is discouraged.)