Theorem 2sb6
Equivalence for double substitution. (Contributed by NM,
3-Feb-2005.)
Conclusion
\( \vdash [ z' / x ] \, [ w' / y ] \, \varphi \leftrightarrow \forall x \, \forall y \, (x = z' \wedge y = w' \rightarrow \varphi) \)
Proof
l0
sb6
\( \vdash [ z' / x ] \, [ w' / y ] \, \varphi \leftrightarrow \forall x \, (x = z' \rightarrow [ w' / y ] \, \varphi) \)
l1
19.21v
\( \vdash \forall y \, (x = z' \rightarrow y = w' \rightarrow \varphi) \leftrightarrow x = z' \rightarrow \forall y \, (y = w' \rightarrow \varphi) \)
impexp
l3
albii _
\( \vdash \forall y \, (x = z' \wedge y = w' \rightarrow \varphi) \leftrightarrow \forall y \, (x = z' \rightarrow y = w' \rightarrow \varphi) \)
sb6
imbi2i _
\( \vdash x = z' \rightarrow [ w' / y ] \, \varphi \leftrightarrow x = z' \rightarrow \forall y \, (y = w' \rightarrow \varphi) \)
3bitr4ri l1 l3 _
albii _
\( \vdash \forall x \, (x = z' \rightarrow [ w' / y ] \, \varphi) \leftrightarrow \forall x \, \forall y \, (x = z' \wedge y = w' \rightarrow \varphi) \)
bitri l0 _