Metamath Proof Explorer

Theorem e2ebindALT

Description: Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axc11n 
 |-  ( A. x x = y -> A. y y = x )
2 nfe1 
 |-  F/ y E. y ph
3 2 19.9 
 |-  ( E. y E. y ph <-> E. y ph )
4 excom 
 |-  ( E. y E. x ph <-> E. x E. y ph )
5 nfa1 
 |-  F/ y A. y y = x
6 id 
 |-  ( A. y y = x -> A. y y = x )
7 biid 
 |-  ( ph <-> ph )
8 7 a1i 
 |-  ( A. y y = x -> ( ph <-> ph ) )
9 8 drex1 
 |-  ( A. y y = x -> ( E. y ph <-> E. x ph ) )
10 6 9 syl 
 |-  ( A. y y = x -> ( E. y ph <-> E. x ph ) )
11 5 10 alrimi 
 |-  ( A. y y = x -> A. y ( E. y ph <-> E. x ph ) )
12 exbi 
 |-  ( A. y ( E. y ph <-> E. x ph ) -> ( E. y E. y ph <-> E. y E. x ph ) )
13 11 12 syl 
 |-  ( A. y y = x -> ( E. y E. y ph <-> E. y E. x ph ) )
14 bitr 
 |-  ( ( ( E. y E. y ph <-> E. y E. x ph ) /\ ( E. y E. x ph <-> E. x E. y ph ) ) -> ( E. y E. y ph <-> E. x E. y ph ) )
15 14 ex 
 |-  ( ( E. y E. y ph <-> E. y E. x ph ) -> ( ( E. y E. x ph <-> E. x E. y ph ) -> ( E. y E. y ph <-> E. x E. y ph ) ) )
16 15 impcom 
 |-  ( ( ( E. y E. x ph <-> E. x E. y ph ) /\ ( E. y E. y ph <-> E. y E. x ph ) ) -> ( E. y E. y ph <-> E. x E. y ph ) )
17 4 13 16 sylancr 
 |-  ( A. y y = x -> ( E. y E. y ph <-> E. x E. y ph ) )
18 bitr3 
 |-  ( ( E. y E. y ph <-> E. x E. y ph ) -> ( ( E. y E. y ph <-> E. y ph ) -> ( E. x E. y ph <-> E. y ph ) ) )
19 18 impcom 
 |-  ( ( ( E. y E. y ph <-> E. y ph ) /\ ( E. y E. y ph <-> E. x E. y ph ) ) -> ( E. x E. y ph <-> E. y ph ) )
20 3 17 19 sylancr 
 |-  ( A. y y = x -> ( E. x E. y ph <-> E. y ph ) )
21 1 20 syl 
 |-  ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )