Theorem mopick

Description: "At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997) (Proof shortened by Wolf Lammen, 17-Sep-2019)

	Ref	Expression
Assertion	mopick	|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		df-mo	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
2		sp	|- ( A. x ( ph -> x = y ) -> ( ph -> x = y ) )
3		pm3.45	|- ( ( ph -> x = y ) -> ( ( ph /\ ps ) -> ( x = y /\ ps ) ) )
4	3	aleximi	|- ( A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> E. x ( x = y /\ ps ) ) )
5		sbalex	|- ( E. x ( x = y /\ ps ) <-> A. x ( x = y -> ps ) )
6		sp	|- ( A. x ( x = y -> ps ) -> ( x = y -> ps ) )
7	5 6	sylbi	|- ( E. x ( x = y /\ ps ) -> ( x = y -> ps ) )
8	4 7	syl6	|- ( A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> ( x = y -> ps ) ) )
9	2 8	syl5d	|- ( A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
10	9	exlimiv	|- ( E. y A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
11	1 10	sylbi	|- ( E* x ph -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
12	11	imp	|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )