Theorem nfbidf
An equality theorem for effectively not free. (Contributed by Mario
Carneiro, 4-Oct-2016.) [df-nf] changed. (Revised by Wolf Lammen,
18-Sep-2021.)
Hypotheses
albid.1
\( \vdash \Finv x \, \varphi \)
albid.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\Finv x \, \psi \leftrightarrow \Finv x \, \chi) \)
Proof
l0
albid.1
albid.2
l2
exbid l0 _
l3
albid.1
albid.2
albid l3 _
l6
imbi12d l2 _
\( \vdash \varphi \rightarrow (\exists x \, \psi \rightarrow \forall x \, \psi \leftrightarrow \exists x \, \chi \rightarrow \forall x \, \chi) \)
l7
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 l6 l7 _