Theorem drex1v

Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drex1 with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 27-Feb-2005.) (Revised by BJ, 17-Jun-2019.)

Hypothesis
dral1v.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
dral1v.1
notbid _
dral1v _
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 _