Description: Obsolete version of sbalex as of 21-Sep-2024. Two equivalent ways of
expressing the proper substitution of y for x in ph , when
x and y are distinct, namely, alternate definitions sb5 and
sb6 . Theorem 6.2 of Quine p. 40. The proof does not involve
df-sb . The implication "to the left" is equs4 and does not require
any disjoint variable condition (but the version with a disjoint
variable condition, equs4v , requires fewer axioms). Theorem
equs45f replaces the disjoint variable condition with a nonfreeness
hypothesis and equs5 replaces it with a distinctor as antecedent.
(Contributed by NM, 14-Apr-2008) Revised to use equsexv in place of
equsex in order to remove dependency on ax-13 . (Revised by BJ, 20-Dec-2020)(Proof modification is discouraged.)(New usage is discouraged.)