Theorem nfbii

Equality theorem for the nonfreeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) [df-nf] changed. (Revised by Wolf Lammen, 12-Sep-2021.)

Hypothesis
nfbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \Finv x \, \psi \)
Proof
l0
nfbiit
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\Finv x \, \varphi \leftrightarrow \Finv x \, \psi) \)
nfbii.1
\( \vdash \varphi \leftrightarrow \psi \)
mpg l0 _