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	⊢ ( ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜓 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		exancom	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) )
2		moeu2	⊢ ( ∃* 𝑥 𝜓 ↔ ( ¬ ∃ 𝑥 𝜓 ∨ ∃! 𝑥 𝜓 ) )
3		19.8a	⊢ ( 𝜓 → ∃ 𝑥 𝜓 )
4	3	con3i	⊢ ( ¬ ∃ 𝑥 𝜓 → ¬ 𝜓 )
5		pm2.21	⊢ ( ¬ 𝜓 → ( 𝜓 → 𝜑 ) )
6	4 5	syl	⊢ ( ¬ ∃ 𝑥 𝜓 → ( 𝜓 → 𝜑 ) )
7	6	a1d	⊢ ( ¬ ∃ 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
8		eupickbi	⊢ ( ∃! 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝜓 → 𝜑 ) ) )
9		sp	⊢ ( ∀ 𝑥 ( 𝜓 → 𝜑 ) → ( 𝜓 → 𝜑 ) )
10	8 9	biimtrdi	⊢ ( ∃! 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
11	7 10	jaoi	⊢ ( ( ¬ ∃ 𝑥 𝜓 ∨ ∃! 𝑥 𝜓 ) → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
12	2 11	sylbi	⊢ ( ∃* 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
13	1 12	biimtrid	⊢ ( ∃* 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜓 → 𝜑 ) ) )
14	13	imp	⊢ ( ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜓 → 𝜑 ) )