Theorem sbbib

Reversal of substitution. (Contributed by AV, 6-Aug-2023.) (Proof shortened by Wolf Lammen, 4-Sep-2023.)

Hypotheses
sbbib.y
\( \vdash \Finv y \, \varphi \)
sbbib.x
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \forall y \, ([ y / x ] \, \varphi \leftrightarrow \psi) \leftrightarrow \forall x \, (\varphi \leftrightarrow [ x / y ] \, \psi) \)
Proof
l0
nfs1v
sbbib.x
l2
nfbi l0 _
l3
sbbib.y
nfs1v
l5
nfbi l3 _
l6
sbequ12r
sbequ12
bibi12d l6 _
cbvalv1 l2 l5 _