Theorem sb8f
Substitution of variable in universal quantifier. Version of sb8 with
a disjoint variable condition, not requiring [ax-10] or [ax-13].
(Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen,
19-Jan-2023.) Avoid [ax-10]. (Revised by SN, 5-Dec-2024.)
Hypothesis
sb8f.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \forall x \, \varphi \leftrightarrow \forall y \, [ y / x ] \, \varphi \)
Proof
sb6
l1
albii _
\( \vdash \forall y \, [ y / x ] \, \varphi \leftrightarrow \forall y \, \forall x \, (x = y \rightarrow \varphi) \)
l2
alcom
\( \vdash \forall y \, \forall x \, (x = y \rightarrow \varphi) \leftrightarrow \forall x \, \forall y \, (x = y \rightarrow \varphi) \)
l3
sb6
\( \vdash [ x / y ] \, \varphi \leftrightarrow \forall y \, (y = x \rightarrow \varphi) \)
sb8f.nf
l5
sbf _
\( \vdash [ x / y ] \, \varphi \leftrightarrow \varphi \)
equcom
imbi1i _
albii _
\( \vdash \forall y \, (y = x \rightarrow \varphi) \leftrightarrow \forall y \, (x = y \rightarrow \varphi) \)
3bitr3ri l3 l5 _
albii _
\( \vdash \forall x \, \forall y \, (x = y \rightarrow \varphi) \leftrightarrow \forall x \, \varphi \)
3bitrri l1 l2 _