Theorem 2moswap
A condition allowing to swap an existential quantifier and at at-most-one
quantifier. Usage of this theorem is discouraged because it depends on
[ax-13]. Use the weaker 2moswapv when possible. (Contributed by NM,
10-Apr-2004.) (New usage is discouraged.)
Conclusion
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists^\ast x \, \exists y \, \varphi \rightarrow \exists^\ast y \, \exists x \, \varphi \)
Proof
nfe1
moexex _
l2
expcom _
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists^\ast x \, \exists y \, \varphi \rightarrow \exists^\ast y \, \exists x \, (\exists y \, \varphi \wedge \varphi) \)
19.8a
pm4.71ri _
exbii _
mobii _
\( \vdash \exists^\ast y \, \exists x \, \varphi \leftrightarrow \exists^\ast y \, \exists x \, (\exists y \, \varphi \wedge \varphi) \)
imbitrrdi l2 _