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 19.8a 
 |-  ( A. x ( ph -> x = y ) -> E. y A. x ( ph -> x = y ) )
6 df-mo 
 |-  ( E* x ph <-> E. y A. x ( ph -> x = y ) )
7 5 6 sylibr 
 |-  ( A. x ( ph -> x = y ) -> E* x ph )
8 4 7 vtoclg 
 |-  ( A e. _V -> ( A. x ( ph -> x = A ) -> E* x ph ) )
9 eqvisset 
 |-  ( x = A -> A e. _V )
10 9 imim2i 
 |-  ( ( ph -> x = A ) -> ( ph -> A e. _V ) )
11 10 con3rr3 
 |-  ( -. A e. _V -> ( ( ph -> x = A ) -> -. ph ) )
12 11 alimdv 
 |-  ( -. A e. _V -> ( A. x ( ph -> x = A ) -> A. x -. ph ) )
13 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
14 nexmo 
 |-  ( -. E. x ph -> E* x ph )
15 13 14 sylbi 
 |-  ( A. x -. ph -> E* x ph )
16 12 15 syl6 
 |-  ( -. A e. _V -> ( A. x ( ph -> x = A ) -> E* x ph ) )
17 8 16 pm2.61i 
 |-  ( A. x ( ph -> x = A ) -> E* x ph )