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