Theorem drsb1

Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, x = y \rightarrow ([ z' / x ] \, \varphi \leftrightarrow [ z' / y ] \, \varphi) \)
Proof
equequ1
l1
sps _
l2
imbi1d _
anbi1d l1
drex1 _
l5
anbi12d l2 _
\( \vdash \forall x \, x = y \rightarrow ((x = z' \rightarrow \varphi) \wedge \exists x \, (x = z' \wedge \varphi) \leftrightarrow (y = z' \rightarrow \varphi) \wedge \exists y \, (y = z' \wedge \varphi)) \)
l6
dfsb1
\( \vdash [ z' / x ] \, \varphi \leftrightarrow (x = z' \rightarrow \varphi) \wedge \exists x \, (x = z' \wedge \varphi) \)
dfsb1
\( \vdash [ z' / y ] \, \varphi \leftrightarrow (y = z' \rightarrow \varphi) \wedge \exists y \, (y = z' \wedge \varphi) \)
3bitr4g l5 l6 _