This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eujustALT

Description: Alternate proof of eujust illustrating the use of dvelim . (Contributed by NM, 11-Mar-2010) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 equequ2 
 |-  ( y = z -> ( x = y <-> x = z ) )
2 1 bibi2d 
 |-  ( y = z -> ( ( ph <-> x = y ) <-> ( ph <-> x = z ) ) )
3 2 albidv 
 |-  ( y = z -> ( A. x ( ph <-> x = y ) <-> A. x ( ph <-> x = z ) ) )
4 3 sps 
 |-  ( A. y y = z -> ( A. x ( ph <-> x = y ) <-> A. x ( ph <-> x = z ) ) )
5 4 drex1 
 |-  ( A. y y = z -> ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) ) )
6 hbnae 
 |-  ( -. A. y y = z -> A. y -. A. y y = z )
7 hbnae 
 |-  ( -. A. y y = z -> A. z -. A. y y = z )
8 6 7 alrimih 
 |-  ( -. A. y y = z -> A. y A. z -. A. y y = z )
9 ax-5 
 |-  ( -. A. x ( ph <-> x = w ) -> A. z -. A. x ( ph <-> x = w ) )
10 equequ2 
 |-  ( w = y -> ( x = w <-> x = y ) )
11 10 bibi2d 
 |-  ( w = y -> ( ( ph <-> x = w ) <-> ( ph <-> x = y ) ) )
12 11 albidv 
 |-  ( w = y -> ( A. x ( ph <-> x = w ) <-> A. x ( ph <-> x = y ) ) )
13 12 notbid 
 |-  ( w = y -> ( -. A. x ( ph <-> x = w ) <-> -. A. x ( ph <-> x = y ) ) )
14 9 13 dvelim 
 |-  ( -. A. z z = y -> ( -. A. x ( ph <-> x = y ) -> A. z -. A. x ( ph <-> x = y ) ) )
15 14 naecoms 
 |-  ( -. A. y y = z -> ( -. A. x ( ph <-> x = y ) -> A. z -. A. x ( ph <-> x = y ) ) )
16 ax-5 
 |-  ( -. A. x ( ph <-> x = w ) -> A. y -. A. x ( ph <-> x = w ) )
17 equequ2 
 |-  ( w = z -> ( x = w <-> x = z ) )
18 17 bibi2d 
 |-  ( w = z -> ( ( ph <-> x = w ) <-> ( ph <-> x = z ) ) )
19 18 albidv 
 |-  ( w = z -> ( A. x ( ph <-> x = w ) <-> A. x ( ph <-> x = z ) ) )
20 19 notbid 
 |-  ( w = z -> ( -. A. x ( ph <-> x = w ) <-> -. A. x ( ph <-> x = z ) ) )
21 16 20 dvelim 
 |-  ( -. A. y y = z -> ( -. A. x ( ph <-> x = z ) -> A. y -. A. x ( ph <-> x = z ) ) )
22 3 notbid 
 |-  ( y = z -> ( -. A. x ( ph <-> x = y ) <-> -. A. x ( ph <-> x = z ) ) )
23 22 a1i 
 |-  ( -. A. y y = z -> ( y = z -> ( -. A. x ( ph <-> x = y ) <-> -. A. x ( ph <-> x = z ) ) ) )
24 15 21 23 cbv2h 
 |-  ( A. y A. z -. A. y y = z -> ( A. y -. A. x ( ph <-> x = y ) <-> A. z -. A. x ( ph <-> x = z ) ) )
25 8 24 syl 
 |-  ( -. A. y y = z -> ( A. y -. A. x ( ph <-> x = y ) <-> A. z -. A. x ( ph <-> x = z ) ) )
26 25 notbid 
 |-  ( -. A. y y = z -> ( -. A. y -. A. x ( ph <-> x = y ) <-> -. A. z -. A. x ( ph <-> x = z ) ) )
27 df-ex 
 |-  ( E. y A. x ( ph <-> x = y ) <-> -. A. y -. A. x ( ph <-> x = y ) )
28 df-ex 
 |-  ( E. z A. x ( ph <-> x = z ) <-> -. A. z -. A. x ( ph <-> x = z ) )
29 26 27 28 3bitr4g 
 |-  ( -. A. y y = z -> ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) ) )
30 5 29 pm2.61i 
 |-  ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) )