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		ax12ev2	|- ( E. x ( x = y /\ ps ) -> ( x = y -> ps ) )
6	4 5	syl6	|- ( A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> ( x = y -> ps ) ) )
7	2 6	syl5d	|- ( A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
8	7	exlimiv	|- ( E. y A. x ( ph -> x = y ) -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
9	1 8	sylbi	|- ( E* x ph -> ( E. x ( ph /\ ps ) -> ( ph -> ps ) ) )
10	9	imp	|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )