= Capture-safe equality replacement
{title2=$x=y\to(\varphi\to\varphi[y/x])$}
Equal variables can replace selected free occurrences in a <first-order formula> if the inserted variable is not captured. Starting with atomic equality replacement, derive symmetry, then prove both replacement directions together by <structural induction>. <Negation> uses the reverse induction implication; implication uses both directions; a <universal quantifier> is handled by instantiation, replacement and <universal generalization rule>[generalization] with a variable fresh for the equality assumptions. Bound occurrences are not replaced as free ones.
Back to article page
