Theorem 2exsb
An equivalent expression for double existence. (Contributed by NM,
2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
Proof
l0
nfv
nfv
l2
2sb8ef l0 _
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \)
2sb6
2exbii _
\( \vdash \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (x = z \wedge y = w \rightarrow \varphi) \)
bitri l2 _