Description: Alternate definition of substitution when variables are disjoint.
Similar to Theorem 6.1 of Quine p. 40. The implication "to the right"
is sb1v and even needs no disjoint variable condition, see sb1 .
Theorem sb5f replaces the disjoint variable condition with a
non-freeness hypothesis. (Contributed by NM, 18-Aug-1993) Shorten
sb56 . (Revised by Wolf Lammen, 4-Sep-2023)