Theorem nfbidv

An equality theorem for nonfreeness. See nfbidf for a version without disjoint variable condition but requiring more axioms. (Contributed by Mario Carneiro, 4-Oct-2016.) Remove dependency on [ax-6], [ax-7], [ax-12] by adapting proof of nfbidf. (Revised by BJ, 25-Sep-2022.)

Hypothesis
albidv.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\Finv x \, \psi \leftrightarrow \Finv x \, \chi) \)
Proof
albidv.1
l1
exbidv _
albidv.1
albidv _
l4
imbi12d l1 _
\( \vdash \varphi \rightarrow (\exists x \, \psi \rightarrow \forall x \, \psi \leftrightarrow \exists x \, \chi \rightarrow \forall x \, \chi) \)
l5
df-nf
\( \vdash \Finv x \, \psi \leftrightarrow \exists x \, \psi \rightarrow \forall x \, \psi \)
df-nf
\( \vdash \Finv x \, \chi \leftrightarrow \exists x \, \chi \rightarrow \forall x \, \chi \)
3bitr4g l4 l5 _