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

Proof

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