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 x x = y x y φ y φ

Proof

Step Hyp Ref Expression
1 biidd y y = x φ φ
2 1 drex1 y y = x y φ x φ
3 2 drex2 y y = x y y φ y x φ
4 excom y x φ x y φ
5 3 4 bitrdi y y = x y y φ x y φ
6 nfe1 y y φ
7 6 19.9 y y φ y φ
8 5 7 bitr3di y y = x x y φ y φ
9 8 aecoms x x = y x y φ y φ