Theorem nfxfrd

A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses
nfbii.1
\( \vdash \varphi \leftrightarrow \psi \)
nfxfrd.2
\( \vdash \chi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \chi \rightarrow \Finv x \, \varphi \)
Proof
l0
nfxfrd.2
\( \vdash \chi \rightarrow \Finv x \, \psi \)
nfbii.1
nfbii _
\( \vdash \Finv x \, \varphi \leftrightarrow \Finv x \, \psi \)
sylibr l0 _