Theorem stdpc7

One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 .) Translated to traditional notation, it can be read: " x = y -> ( ph ( x , x ) -> ph ( x , y ) ), provided that \( y \) is free for \( x' \) in ph ( x , x ) ". Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.)

Conclusion
\( \vdash x' = y \rightarrow [ x' / y ] \, \varphi \rightarrow \varphi \)
Proof
sbequ2
equcoms _