Theorem sbequ12r

An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Conclusion

\( \vdash x' = y \rightarrow ([ x' / y ] \, \varphi \leftrightarrow \varphi) \)

Proof

sbequ12

bicomd _

equcoms _