Metamath Proof Explorer


Theorem e2ebind

Description: Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. e2ebind is derived from e2ebindVD . (Contributed by Alan Sare, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion e2ebind
|- ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )

Proof

Step Hyp Ref Expression
1 biidd
 |-  ( A. y y = x -> ( ph <-> ph ) )
2 1 drex1
 |-  ( A. y y = x -> ( E. y ph <-> E. x ph ) )
3 2 drex2
 |-  ( A. y y = x -> ( E. y E. y ph <-> E. y E. x ph ) )
4 excom
 |-  ( E. y E. x ph <-> E. x E. y ph )
5 3 4 bitrdi
 |-  ( A. y y = x -> ( E. y E. y ph <-> E. x E. y ph ) )
6 nfe1
 |-  F/ y E. y ph
7 6 19.9
 |-  ( E. y E. y ph <-> E. y ph )
8 5 7 bitr3di
 |-  ( A. y y = x -> ( E. x E. y ph <-> E. y ph ) )
9 8 aecoms
 |-  ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )