Theorem eeor
Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994.)
Avoid [ax-10]. (Revised by GG, 21-Nov-2024.)
Hypotheses
eeor.1
\( \vdash \Finv y \, \varphi \)
eeor.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \exists x \, \exists y \, (\varphi \vee \psi) \leftrightarrow \exists x \, \varphi \vee \exists y \, \psi \)
Proof
19.43
l1
exbii _
\( \vdash \exists x \, \exists y \, (\varphi \vee \psi) \leftrightarrow \exists x \, (\exists y \, \varphi \vee \exists y \, \psi) \)
l2
19.43
\( \vdash \exists x \, (\exists y \, \varphi \vee \exists y \, \psi) \leftrightarrow \exists x \, \exists y \, \varphi \vee \exists x \, \exists y \, \psi \)
eeor.1
19.9 _
l5
exbii _
l6
excom
\( \vdash \exists x \, \exists y \, \psi \leftrightarrow \exists y \, \exists x \, \psi \)
eeor.2
19.9 _
exbii _
\( \vdash \exists y \, \exists x \, \psi \leftrightarrow \exists y \, \psi \)
bitri l6 _
orbi12i l5 _
\( \vdash \exists x \, \exists y \, \varphi \vee \exists x \, \exists y \, \psi \leftrightarrow \exists x \, \varphi \vee \exists y \, \psi \)
bitri l2 _
\( \vdash \exists x \, (\exists y \, \varphi \vee \exists y \, \psi) \leftrightarrow \exists x \, \varphi \vee \exists y \, \psi \)
bitri l1 _