Theorem 2sb5
Equivalence for double substitution. (Contributed by NM,
3-Feb-2005.)
Conclusion
\( \vdash [ z' / x ] \, [ w' / y ] \, \varphi \leftrightarrow \exists x \, \exists y \, (x = z' \wedge y = w' \wedge \varphi) \)
Proof
l0
sb5
\( \vdash [ z' / x ] \, [ w' / y ] \, \varphi \leftrightarrow \exists x \, (x = z' \wedge [ w' / y ] \, \varphi) \)
l1
19.42v
\( \vdash \exists y \, (x = z' \wedge (y = w' \wedge \varphi)) \leftrightarrow x = z' \wedge \exists y \, (y = w' \wedge \varphi) \)
anass
l3
exbii _
\( \vdash \exists y \, (x = z' \wedge y = w' \wedge \varphi) \leftrightarrow \exists y \, (x = z' \wedge (y = w' \wedge \varphi)) \)
sb5
anbi2i _
\( \vdash x = z' \wedge [ w' / y ] \, \varphi \leftrightarrow x = z' \wedge \exists y \, (y = w' \wedge \varphi) \)
3bitr4ri l1 l3 _
exbii _
\( \vdash \exists x \, (x = z' \wedge [ w' / y ] \, \varphi) \leftrightarrow \exists x \, \exists y \, (x = z' \wedge y = w' \wedge \varphi) \)
bitri l0 _