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

Metamath Proof Explorer

Theorem mo2icl

Description: Theorem for inferring "at most one". (Contributed by NM, 17-Oct-1996)

Ref Expression
Assertion mo2icl 
|- ( A. x ( ph -> x = A ) -> E* x ph )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( y = A -> ( x = y <-> x = A ) )
2 1 imbi2d 
 |-  ( y = A -> ( ( ph -> x = y ) <-> ( ph -> x = A ) ) )
3 2 albidv 
 |-  ( y = A -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = A ) ) )
4 3 imbi1d 
 |-  ( y = A -> ( ( A. x ( ph -> x = y ) -> E* x ph ) <-> ( A. x ( ph -> x = A ) -> E* x ph ) ) )
5 equequ2 
 |-  ( y = z -> ( x = y <-> x = z ) )
6 5 imbi2d 
 |-  ( y = z -> ( ( ph -> x = y ) <-> ( ph -> x = z ) ) )
7 6 albidv 
 |-  ( y = z -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = z ) ) )
8 7 19.8aw 
 |-  ( A. x ( ph -> x = y ) -> E. y A. x ( ph -> x = y ) )
9 df-mo 
 |-  ( E* x ph <-> E. y A. x ( ph -> x = y ) )
10 8 9 sylibr 
 |-  ( A. x ( ph -> x = y ) -> E* x ph )
11 4 10 vtoclg 
 |-  ( A e. _V -> ( A. x ( ph -> x = A ) -> E* x ph ) )
12 eqvisset 
 |-  ( x = A -> A e. _V )
13 12 imim2i 
 |-  ( ( ph -> x = A ) -> ( ph -> A e. _V ) )
14 13 con3rr3 
 |-  ( -. A e. _V -> ( ( ph -> x = A ) -> -. ph ) )
15 14 alimdv 
 |-  ( -. A e. _V -> ( A. x ( ph -> x = A ) -> A. x -. ph ) )
16 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
17 nexmo 
 |-  ( -. E. x ph -> E* x ph )
18 16 17 sylbi 
 |-  ( A. x -. ph -> E* x ph )
19 15 18 syl6 
 |-  ( -. A e. _V -> ( A. x ( ph -> x = A ) -> E* x ph ) )
20 11 19 pm2.61i 
 |-  ( A. x ( ph -> x = A ) -> E* x ph )