Theorem dral1v

Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 with a disjoint variable condition, which does not require [ax-13]. Remark: the corresponding versions for dral2 and drex2 are instances of albidv and exbidv respectively. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v. (Revised by Wolf Lammen, 30-Mar-2024.) Avoid [ax-10]. (Revised by GG, 18-Nov-2024.)

Hypothesis
dral1v.1
\( \vdash \forall x \, x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, x = y \rightarrow (\forall x \, \varphi \leftrightarrow \forall y \, \psi) \)
Proof
l0
ax-5
\( \vdash \forall x \, x = y \rightarrow \forall x \, \forall x \, x = y \)
l1
dral1v.1
l2
albidh l0 _
\( \vdash \forall x \, x = y \rightarrow (\forall x \, \varphi \leftrightarrow \forall x \, \psi) \)
l3
axc11v
l4
axc11rv
l5
impbid l3 _
\( \vdash \forall x \, x = y \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \psi) \)
l6
bitrd l2 _