Theorem mopickr

Description: "At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 ( pm2.21 ) and *14.26 ( eupickbi ) from WhiteheadRussell p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		exancom	|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
2		moeu2	|- ( E* x ps <-> ( -. E. x ps \/ E! x ps ) )
3		19.8a	|- ( ps -> E. x ps )
4	3	con3i	|- ( -. E. x ps -> -. ps )
5		pm2.21	|- ( -. ps -> ( ps -> ph ) )
6	4 5	syl	|- ( -. E. x ps -> ( ps -> ph ) )
7	6	a1d	|- ( -. E. x ps -> ( E. x ( ps /\ ph ) -> ( ps -> ph ) ) )
8		eupickbi	|- ( E! x ps -> ( E. x ( ps /\ ph ) <-> A. x ( ps -> ph ) ) )
9		sp	|- ( A. x ( ps -> ph ) -> ( ps -> ph ) )
10	8 9	biimtrdi	|- ( E! x ps -> ( E. x ( ps /\ ph ) -> ( ps -> ph ) ) )
11	7 10	jaoi	|- ( ( -. E. x ps \/ E! x ps ) -> ( E. x ( ps /\ ph ) -> ( ps -> ph ) ) )
12	2 11	sylbi	|- ( E* x ps -> ( E. x ( ps /\ ph ) -> ( ps -> ph ) ) )
13	1 12	biimtrid	|- ( E* x ps -> ( E. x ( ph /\ ps ) -> ( ps -> ph ) ) )
14	13	imp	|- ( ( E* x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) )