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	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to (φ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		df-mo	$⊢ \exists^{*} x φ \leftrightarrow \exists y \forall x (φ \to x = y)$
2		sp	$⊢ \forall x (φ \to x = y) \to (φ \to x = y)$
3		pm3.45	$⊢ (φ \to x = y) \to ((φ \land ψ) \to (x = y \land ψ))$
4	3	aleximi	$⊢ \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to \exists x (x = y \land ψ))$
5		sbalex	$⊢ \exists x (x = y \land ψ) \leftrightarrow \forall x (x = y \to ψ)$
6		sp	$⊢ \forall x (x = y \to ψ) \to (x = y \to ψ)$
7	5 6	sylbi	$⊢ \exists x (x = y \land ψ) \to (x = y \to ψ)$
8	4 7	syl6	$⊢ \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to (x = y \to ψ))$
9	2 8	syl5d	$⊢ \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to (φ \to ψ))$
10	9	exlimiv	$⊢ \exists y \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to (φ \to ψ))$
11	1 10	sylbi	$⊢ \exists^{*} x φ \to (\exists x (φ \land ψ) \to (φ \to ψ))$
12	11	imp	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to (φ \to ψ)$