Theorem
sbbibvv
Reversal of substitution. (Contributed by AV, 6-Aug-2023.)
Conclusion
\( \vdash \forall y \, ([ y / x ] \, \varphi \leftrightarrow \psi) \leftrightarrow \forall x \, (\varphi \leftrightarrow [ x / y ] \, \psi) \)
Proof
l0
nfv
nfv
sbbib
l0
_
This is the content in the right pane.