Theorem drsb2

Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.)

Conclusion

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

Proof

sbequ

sps _