Theorem 2sb8ef
An equivalent expression for double existence. Version of 2sb8e with
more disjoint variable conditions, not requiring [ax-13]. (Contributed
by Wolf Lammen, 28-Jan-2023.)
Hypotheses
2sb8ef.1
\( \vdash \Finv w \, \varphi \)
2sb8ef.2
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, [ z / x ] \, [ w / y ] \, \varphi \)
Proof
2sb8ef.1
sb8ef _
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 \)
2sb8ef.2
nfsbv _
sb8ef _
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 _