This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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		ax12ev2	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜓 ) → ( 𝑥 = 𝑦 → 𝜓 ) )
6	4 5	syl6	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝑥 = 𝑦 → 𝜓 ) ) )
7	2 6	syl5d	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
8	7	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
9	1 8	sylbi	⊢ ( ∃* 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
10	9	imp	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )