Theorem dral1ALT

Alternate proof of dral1, shorter but requiring [ax-11]. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

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