Theorem ich2ex

Description: Two setvar variables are always interchangeable when there are two existential quantifiers. (Contributed by SN, 23-Nov-2023)

	Ref	Expression
Assertion	ich2ex	$$⊢\left[x\rightleftarrows y\right]\exists x\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfe1	$$⊢Ⅎx\exists x\exists y\phi$$
2		excom	$$⊢\exists x\exists y\phi \leftrightarrow \exists y\exists x\phi$$
3		nfe1	$$⊢Ⅎy\exists y\exists x\phi$$
4	2 3	nfxfr	$$⊢Ⅎy\exists x\exists y\phi$$
5	1 4	ichf	$$⊢\left[x\rightleftarrows y\right]\exists x\exists y\phi$$