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

Proof

Step	Hyp	Ref	Expression
1		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
2		sp	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
3		pm3.45	⊢ ( ( 𝜑 → 𝑥 = 𝑦 ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 = 𝑦 ∧ 𝜓 ) ) )
4	3	aleximi	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜓 ) ) )
5		sb56	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) )
6		sp	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) → ( 𝑥 = 𝑦 → 𝜓 ) )
7	5 6	sylbi	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜓 ) → ( 𝑥 = 𝑦 → 𝜓 ) )
8	4 7	syl6	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝑥 = 𝑦 → 𝜓 ) ) )
9	2 8	syl5d	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
10	9	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
11	1 10	sylbi	⊢ ( ∃* 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
12	11	imp	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )