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 )