Theorem drnf2

Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.) Usage of this theorem is discouraged because it depends on [ax-13]. Use nfbidv 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 z \, \varphi \leftrightarrow \Finv z \, \psi) \)
Proof
l0
nfae
dral1.1
nfbidf l0 _