Theorem eeor

Description: Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994) Avoid ax-10 . (Revised by GG, 21-Nov-2024)

	Ref	Expression
Hypotheses	eeor.1	$$⊢Ⅎy\phi$$
	eeor.2	$$⊢Ⅎx\psi$$
Assertion	eeor	$$⊢\exists x\exists y\left(\phi \vee \psi \right)\leftrightarrow \left(\exists x\phi \vee \exists y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eeor.1	$$⊢Ⅎy\phi$$
2		eeor.2	$$⊢Ⅎx\psi$$
3		19.43	$$⊢\exists y\left(\phi \vee \psi \right)\leftrightarrow \left(\exists y\phi \vee \exists y\psi \right)$$
4	3	exbii	$$⊢\exists x\exists y\left(\phi \vee \psi \right)\leftrightarrow \exists x\left(\exists y\phi \vee \exists y\psi \right)$$
5		19.43	$$⊢\exists x\left(\exists y\phi \vee \exists y\psi \right)\leftrightarrow \left(\exists x\exists y\phi \vee \exists x\exists y\psi \right)$$
6	1	19.9	$$⊢\exists y\phi \leftrightarrow \phi$$
7	6	exbii	$$⊢\exists x\exists y\phi \leftrightarrow \exists x\phi$$
8		excom	$$⊢\exists x\exists y\psi \leftrightarrow \exists y\exists x\psi$$
9	2	19.9	$$⊢\exists x\psi \leftrightarrow \psi$$
10	9	exbii	$$⊢\exists y\exists x\psi \leftrightarrow \exists y\psi$$
11	8 10	bitri	$$⊢\exists x\exists y\psi \leftrightarrow \exists y\psi$$
12	7 11	orbi12i	$$⊢\left(\exists x\exists y\phi \vee \exists x\exists y\psi \right)\leftrightarrow \left(\exists x\phi \vee \exists y\psi \right)$$
13	5 12	bitri	$$⊢\exists x\left(\exists y\phi \vee \exists y\psi \right)\leftrightarrow \left(\exists x\phi \vee \exists y\psi \right)$$
14	4 13	bitri	$$⊢\exists x\exists y\left(\phi \vee \psi \right)\leftrightarrow \left(\exists x\phi \vee \exists y\psi \right)$$