Theorem 2sb8e
An equivalent expression for double existence. Usage of this theorem is
discouraged because it depends on [ax-13]. For a version requiring
more disjoint variables, but fewer axioms, see 2sb8ef. (Contributed
by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \)
Proof
nfv
sb8e _
l2
exbii _
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists x \, \exists w \, [ w / y ] \, \varphi \)
excom
\( \vdash \exists x \, \exists w \, [ w / y ] \, \varphi \leftrightarrow \exists w \, \exists x \, [ w / y ] \, \varphi \)
l4
bitri l2 _
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists w \, \exists x \, [ w / y ] \, \varphi \)
nfv
nfsb _
sb8e _
l8
exbii _
\( \vdash \exists w \, \exists x \, [ w / y ] \, \varphi \leftrightarrow \exists w \, \exists z \, [ z / x ] \, [ w / y ] \, \varphi \)
excom
\( \vdash \exists w \, \exists z \, [ z / x ] \, [ w / y ] \, \varphi \leftrightarrow \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \)
3bitri l4 l8 _