Theorem sbrim
Substitution in an implication with a variable not free in the
antecedent affects only the consequent. (Contributed by NM,
2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Avoid [ax-10].
(Revised by GG, 20-Nov-2024.)
Hypothesis
sbrim.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / x ] \, \psi \)
Proof
bi2.04
l1
albii _
\( \vdash \forall x \, (x = t \rightarrow \varphi \rightarrow \psi) \leftrightarrow \forall x \, (\varphi \rightarrow x = t \rightarrow \psi) \)
sbrim.1
19.21 _
\( \vdash \forall x \, (\varphi \rightarrow x = t \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, (x = t \rightarrow \psi) \)
bitri l1 _
l5
imbi2i _
\( \vdash t = y' \rightarrow \forall x \, (x = t \rightarrow \varphi \rightarrow \psi) \leftrightarrow t = y' \rightarrow \varphi \rightarrow \forall x \, (x = t \rightarrow \psi) \)
bi2.04
\( \vdash t = y' \rightarrow \varphi \rightarrow \forall x \, (x = t \rightarrow \psi) \leftrightarrow \varphi \rightarrow t = y' \rightarrow \forall x \, (x = t \rightarrow \psi) \)
bitri l5 _
l8
albii _
\( \vdash \forall t \, (t = y' \rightarrow \forall x \, (x = t \rightarrow \varphi \rightarrow \psi)) \leftrightarrow \forall t \, (\varphi \rightarrow t = y' \rightarrow \forall x \, (x = t \rightarrow \psi)) \)
l9
dfsb
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \forall t \, (t = y' \rightarrow \forall x \, (x = t \rightarrow \varphi \rightarrow \psi)) \)
dfsb
l11
imbi2i _
\( \vdash \varphi \rightarrow [ y' / x ] \, \psi \leftrightarrow \varphi \rightarrow \forall t \, (t = y' \rightarrow \forall x \, (x = t \rightarrow \psi)) \)
19.21v
\( \vdash \forall t \, (\varphi \rightarrow t = y' \rightarrow \forall x \, (x = t \rightarrow \psi)) \leftrightarrow \varphi \rightarrow \forall t \, (t = y' \rightarrow \forall x \, (x = t \rightarrow \psi)) \)
bitr4i l11 _
\( \vdash \varphi \rightarrow [ y' / x ] \, \psi \leftrightarrow \forall t \, (\varphi \rightarrow t = y' \rightarrow \forall x \, (x = t \rightarrow \psi)) \)
3bitr4i l8 l9 _