This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ [x ⇄ y] \exists x \exists y φ$

Step	Hyp	Ref	Expression
1		nfe1	$⊢ Ⅎ x \exists x \exists y φ$
2		excom	$⊢ \exists x \exists y φ \leftrightarrow \exists y \exists x φ$
3		nfe1	$⊢ Ⅎ y \exists y \exists x φ$
4	2 3	nfxfr	$⊢ Ⅎ y \exists x \exists y φ$
5	1 4	ichf	$⊢ [x ⇄ y] \exists x \exists y φ$