Theorem drnf1

Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on [ax-13]. Use drnf1v instead. (New usage is discouraged.)

Hypothesis
dral1.1
\( \vdash \forall x \, x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, x = y \rightarrow (\Finv x \, \varphi \leftrightarrow \Finv y \, \psi) \)
Proof
l0
dral1.1
dral1.1
dral1 _
imbi12d l0 _
l4
dral1 _
\( \vdash \forall x \, x = y \rightarrow (\forall x \, (\varphi \rightarrow \forall x \, \varphi) \leftrightarrow \forall y \, (\psi \rightarrow \forall y \, \psi)) \)
l5
nf5
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, (\varphi \rightarrow \forall x \, \varphi) \)
nf5
\( \vdash \Finv y \, \psi \leftrightarrow \forall y \, (\psi \rightarrow \forall y \, \psi) \)
3bitr4g l4 l5 _