Metamath Proof Explorer

Theorem e2ebindVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. e2ebind is e2ebindVD without virtual deductions and was automatically derived from e2ebindVD .

1:: |- ( ph <-> ph )
2:1: |- ( A. y y = x -> ( ph <-> ph ) )
3:2: |- ( A. y y = x -> ( E. y ph <-> E. x ph ) )
4:: |- (. A. y y = x ->. A. y y = x ).
5:3,4: |- (. A. y y = x ->. ( E. y ph <-> E. x ph ) ).
6:: |- ( A. y y = x -> A. y A. y y = x )
7:5,6: |- (. A. y y = x ->. A. y ( E. y ph <-> E. x ph ) ).
8:7: |- (. A. y y = x ->. ( E. y E. y ph <-> E. y E. x ph ) ).
9:: |- ( E. y E. x ph <-> E. x E. y ph )
10:8,9: |- (. A. y y = x ->. ( E. y E. y ph <-> E. x E. y ph ) ).
11:: |- ( E. y ph -> A. y E. y ph )
12:11: |- ( E. y E. y ph <-> E. y ph )
13:10,12: |- (. A. y y = x ->. ( E. x E. y ph <-> E. y ph ) ).
14:13: |- ( A. y y = x -> ( E. x E. y ph <-> E. y ph ) )
15:: |- ( A. y y = x <-> A. x x = y )
qed:14,15: |- ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )
(Contributed by Alan Sare, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion e2ebindVD 
|- ( 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 hba1 
 |-  ( A. y y = x -> A. y A. y y = x )
3 idn1 
 |-  (. A. y y = x ->. A. y y = x ).
4 biid 
 |-  ( ph <-> ph )
5 4 a1i 
 |-  ( A. y y = x -> ( ph <-> ph ) )
6 5 drex1 
 |-  ( A. y y = x -> ( E. y ph <-> E. x ph ) )
7 3 6 e1a 
 |-  (. A. y y = x ->. ( E. y ph <-> E. x ph ) ).
8 2 7 gen11nv 
 |-  (. A. y y = x ->. A. y ( E. y ph <-> E. x ph ) ).
9 exbi 
 |-  ( A. y ( E. y ph <-> E. x ph ) -> ( E. y E. y ph <-> E. y E. x ph ) )
10 8 9 e1a 
 |-  (. A. y y = x ->. ( E. y E. y ph <-> E. y E. x ph ) ).
11 excom 
 |-  ( E. y E. x ph <-> E. x E. y ph )
12 bibi1 
 |-  ( ( E. y E. y ph <-> E. y E. x ph ) -> ( ( E. y E. y ph <-> E. x E. y ph ) <-> ( E. y E. x ph <-> E. x E. y ph ) ) )
13 12 biimprd 
 |-  ( ( 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 ) ) )
14 10 11 13 e10 
 |-  (. A. y y = x ->. ( E. y E. y ph <-> E. x E. y ph ) ).
15 nfe1 
 |-  F/ y E. y ph
16 15 19.9 
 |-  ( E. y E. y ph <-> E. y ph )
17 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 ) ) )
18 14 16 17 e10 
 |-  (. A. y y = x ->. ( E. x E. y ph <-> E. y ph ) ).
19 18 in1 
 |-  ( A. y y = x -> ( E. x E. y ph <-> E. y ph ) )
20 1 19 syl 
 |-  ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )