Theorem nfxfr

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

Hypotheses
nfbii.1
\( \vdash \varphi \leftrightarrow \psi \)
nfxfr.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, \varphi \)
Proof
l0
nfxfr.2
\( \vdash \Finv x \, \psi \)
nfbii.1
nfbii _
\( \vdash \Finv x \, \varphi \leftrightarrow \Finv x \, \psi \)
mpbir l0 _