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	⊢ [ 𝑥 ⇄ 𝑦 ] ∃ 𝑥 ∃ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∃ 𝑦 𝜑
2		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 𝜑 )
3		nfe1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∃ 𝑥 𝜑
4	2 3	nfxfr	⊢ Ⅎ 𝑦 ∃ 𝑥 ∃ 𝑦 𝜑
5	1 4	ichf	⊢ [ 𝑥 ⇄ 𝑦 ] ∃ 𝑥 ∃ 𝑦 𝜑