Theorem sbnf2
Two ways of expressing " \( x \) is (effectively) not free in \( \varphi \) ".
(Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario
Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Sep-2018.)
Avoid [ax-13]. (Revised by Wolf Lammen, 30-Jan-2023.)
Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \forall y \, \forall z \, ([ y / x ] \, \varphi \leftrightarrow [ z / x ] \, \varphi) \)
Proof
nfv
l1
sb8ef _
sb8v
l3
imbi12i l1 _
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \varphi \leftrightarrow \exists y \, [ y / x ] \, \varphi \rightarrow \forall z \, [ z / x ] \, \varphi \)
l4
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
pm11.53v
\( \vdash \forall y \, \forall z \, ([ y / x ] \, \varphi \rightarrow [ z / x ] \, \varphi) \leftrightarrow \exists y \, [ y / x ] \, \varphi \rightarrow \forall z \, [ z / x ] \, \varphi \)
l6
3bitr4i l3 l4 _
nfv
l8
sb8ef _
sb8v
l10
imbi12i l8 _
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \varphi \leftrightarrow \exists z \, [ z / x ] \, \varphi \rightarrow \forall y \, [ y / x ] \, \varphi \)
pm11.53v
\( \vdash \forall z \, \forall y \, ([ z / x ] \, \varphi \rightarrow [ y / x ] \, \varphi) \leftrightarrow \exists z \, [ z / x ] \, \varphi \rightarrow \forall y \, [ y / x ] \, \varphi \)
l12
3bitr4i l10 l4 _
\( \vdash \Finv x \, \varphi \leftrightarrow \forall z \, \forall y \, ([ z / x ] \, \varphi \rightarrow [ y / x ] \, \varphi) \)
alcom
\( \vdash \forall z \, \forall y \, ([ z / x ] \, \varphi \rightarrow [ y / x ] \, \varphi) \leftrightarrow \forall y \, \forall z \, ([ z / x ] \, \varphi \rightarrow [ y / x ] \, \varphi) \)
bitri l12 _
l15
anbi12i l6 _
\( \vdash \Finv x \, \varphi \wedge \Finv x \, \varphi \leftrightarrow \forall y \, \forall z \, ([ y / x ] \, \varphi \rightarrow [ z / x ] \, \varphi) \wedge \forall y \, \forall z \, ([ z / x ] \, \varphi \rightarrow [ y / x ] \, \varphi) \)
l16
pm4.24
\( \vdash \Finv x \, \varphi \leftrightarrow \Finv x \, \varphi \wedge \Finv x \, \varphi \)
2albiim
\( \vdash \forall y \, \forall z \, ([ y / x ] \, \varphi \leftrightarrow [ z / x ] \, \varphi) \leftrightarrow \forall y \, \forall z \, ([ y / x ] \, \varphi \rightarrow [ z / x ] \, \varphi) \wedge \forall y \, \forall z \, ([ z / x ] \, \varphi \rightarrow [ y / x ] \, \varphi) \)
3bitr4i l15 l16 _