Theorem 2moswapv
A condition allowing to swap an existential quantifier and at
at-most-one quantifier. Version of 2moswap with a disjoint variable
condition, which does not require [ax-13]. (Contributed by NM,
10-Apr-2004.) (Revised by GG, 22-Aug-2023.) Factor out common proof
lines with moexexvw. (Revised by Wolf Lammen, 2-Oct-2023.)
Conclusion
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists^\ast x \, \exists y \, \varphi \rightarrow \exists^\ast y \, \exists x \, \varphi \)
Proof
l0
nfe1
l1
nfmov _
nfe1
nfmov _
moexexlem l0 l1 _
l5
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 l5 _