Theorem sbnf
Move nonfree predicate in and out of substitution; see sbal and
sbex. (Contributed by BJ, 2-May-2019.) (Proof shortened by Wolf
Lammen, 2-May-2025.)
Conclusion
\( \vdash [ z' / y ] \, \Finv x \, \varphi \leftrightarrow \Finv x \, [ z' / y ] \, \varphi \)
Proof
df-nf
l1
sbbii _
\( \vdash [ z' / y ] \, \Finv x \, \varphi \leftrightarrow [ z' / y ] \, (\exists x \, \varphi \rightarrow \forall x \, \varphi) \)
l2
sbim
\( \vdash [ z' / y ] \, (\exists x \, \varphi \rightarrow \forall x \, \varphi) \leftrightarrow [ z' / y ] \, \exists x \, \varphi \rightarrow [ z' / y ] \, \forall x \, \varphi \)
l3
sbex
sbal
l5
imbi12i l3 _
\( \vdash [ z' / y ] \, \exists x \, \varphi \rightarrow [ z' / y ] \, \forall x \, \varphi \leftrightarrow \exists x \, [ z' / y ] \, \varphi \rightarrow \forall x \, [ z' / y ] \, \varphi \)
df-nf
\( \vdash \Finv x \, [ z' / y ] \, \varphi \leftrightarrow \exists x \, [ z' / y ] \, \varphi \rightarrow \forall x \, [ z' / y ] \, \varphi \)
bitr4i l5 _
\( \vdash [ z' / y ] \, \exists x \, \varphi \rightarrow [ z' / y ] \, \forall x \, \varphi \leftrightarrow \Finv x \, [ z' / y ] \, \varphi \)
3bitri l1 l2 _