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		dfmo	$⊢ \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		ax12ev2	$⊢ \exists x (x = y \land ψ) \to (x = y \to ψ)$
6	4 5	syl6	$⊢ \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to (x = y \to ψ))$
7	2 6	syl5d	$⊢ \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to (φ \to ψ))$
8	7	exlimiv	$⊢ \exists y \forall x (φ \to x = y) \to (\exists x (φ \land ψ) \to (φ \to ψ))$
9	1 8	sylbi	$⊢ \exists^{*} x φ \to (\exists x (φ \land ψ) \to (φ \to ψ))$
10	9	imp	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to (φ \to ψ)$