Theorem sb8v
Substitution of variable in universal quantifier. Version of sb8f
with a disjoint variable condition replacing the nonfree hypothesis
\( \Finv y \, \varphi \), not requiring [ax-12]. (Contributed by SN,
5-Dec-2024.)
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) \)
equcom
imbi1i _
l5
albii _
\( \vdash \forall y \, (x = y \rightarrow \varphi) \leftrightarrow \forall y \, (y = x \rightarrow \varphi) \)
equsv
\( \vdash \forall y \, (y = x \rightarrow \varphi) \leftrightarrow \varphi \)
bitri l5 _
albii _
\( \vdash \forall x \, \forall y \, (x = y \rightarrow \varphi) \leftrightarrow \forall x \, \varphi \)
3bitrri l1 l2 _