Theorem eqeu

Description: A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009)

	Ref	Expression
Hypothesis	eqeu.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	eqeu	|- ( ( A e. B /\ ps /\ A. x ( ph -> x = A ) ) -> E! x ph )

Proof

Step	Hyp	Ref	Expression
1		eqeu.1	|- ( x = A -> ( ph <-> ps ) )
2	1	spcegv	|- ( A e. B -> ( ps -> E. x ph ) )
3	2	imp	|- ( ( A e. B /\ ps ) -> E. x ph )
4	3	3adant3	|- ( ( A e. B /\ ps /\ A. x ( ph -> x = A ) ) -> E. x ph )
5		eqeq2	|- ( y = A -> ( x = y <-> x = A ) )
6	5	imbi2d	|- ( y = A -> ( ( ph -> x = y ) <-> ( ph -> x = A ) ) )
7	6	albidv	|- ( y = A -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = A ) ) )
8	7	spcegv	|- ( A e. B -> ( A. x ( ph -> x = A ) -> E. y A. x ( ph -> x = y ) ) )
9	8	imp	|- ( ( A e. B /\ A. x ( ph -> x = A ) ) -> E. y A. x ( ph -> x = y ) )
10	9	3adant2	|- ( ( A e. B /\ ps /\ A. x ( ph -> x = A ) ) -> E. y A. x ( ph -> x = y ) )
11		eu3v	|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
12	4 10 11	sylanbrc	|- ( ( A e. B /\ ps /\ A. x ( ph -> x = A ) ) -> E! x ph )