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 ] E. x E. y ph

Proof

Step Hyp Ref Expression
1 nfe1 
 |-  F/ x E. x E. y ph
2 excom 
 |-  ( E. x E. y ph <-> E. y E. x ph )
3 nfe1 
 |-  F/ y E. y E. x ph
4 2 3 nfxfr 
 |-  F/ y E. x E. y ph
5 1 4 ichf 
 |-  [ x <> y ] E. x E. y ph