Theorem nfbiit

Equivalence theorem for the nonfreeness predicate. Closed form of nfbii. (Contributed by Giovanni Mascellani, 10-Apr-2018.) Reduce axiom usage. (Revised by BJ, 6-May-2019.)

Conclusion
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\Finv x \, \varphi \leftrightarrow \Finv x \, \psi) \)
Proof
l0
exbi
albi
l2
imbi12d l0 _
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \varphi \leftrightarrow \exists x \, \psi \rightarrow \forall x \, \psi) \)
l3
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
df-nf
\( \vdash \Finv x \, \psi \leftrightarrow \exists x \, \psi \rightarrow \forall x \, \psi \)
3bitr4g l2 l3 _