Theorem drex1

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]. Use the weaker drex1v if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)

Hypothesis
dral1.1
\( \vdash \forall x \, x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, x = y \rightarrow (\exists x \, \varphi \leftrightarrow \exists y \, \psi) \)
Proof
dral1.1
notbid _
dral1 _
l3
notbid _
\( \vdash \forall x \, x = y \rightarrow (\neg \forall x \, \neg \varphi \leftrightarrow \neg \forall y \, \neg \psi) \)
l4
df-ex
\( \vdash \exists x \, \varphi \leftrightarrow \neg \forall x \, \neg \varphi \)
df-ex
\( \vdash \exists y \, \psi \leftrightarrow \neg \forall y \, \neg \psi \)
3bitr4g l3 l4 _