mopickr

Description: "At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 ( pm2.21 ) and *14.26 ( eupickbi ) from WhiteheadRussell p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	mopickr	$⊢ (\exists^{*} x ψ \land \exists x (φ \land ψ)) \to (ψ \to φ)$

Proof

Step	Hyp	Ref	Expression
1		exancom	$⊢ \exists x (φ \land ψ) \leftrightarrow \exists x (ψ \land φ)$
2		moeu2	$⊢ \exists^{*} x ψ \leftrightarrow (\neg \exists x ψ \lor \exists! x ψ)$
3		19.8a	$⊢ ψ \to \exists x ψ$
4	3	con3i	$⊢ \neg \exists x ψ \to \neg ψ$
5		pm2.21	$⊢ \neg ψ \to (ψ \to φ)$
6	4 5	syl	$⊢ \neg \exists x ψ \to (ψ \to φ)$
7	6	a1d	$⊢ \neg \exists x ψ \to (\exists x (ψ \land φ) \to (ψ \to φ))$
8		eupickbi	$⊢ \exists! x ψ \to (\exists x (ψ \land φ) \leftrightarrow \forall x (ψ \to φ))$
9		sp	$⊢ \forall x (ψ \to φ) \to (ψ \to φ)$
10	8 9	biimtrdi	$⊢ \exists! x ψ \to (\exists x (ψ \land φ) \to (ψ \to φ))$
11	7 10	jaoi	$⊢ (\neg \exists x ψ \lor \exists! x ψ) \to (\exists x (ψ \land φ) \to (ψ \to φ))$
12	2 11	sylbi	$⊢ \exists^{*} x ψ \to (\exists x (ψ \land φ) \to (ψ \to φ))$
13	1 12	biimtrid	$⊢ \exists^{*} x ψ \to (\exists x (φ \land ψ) \to (ψ \to φ))$
14	13	imp	$⊢ (\exists^{*} x ψ \land \exists x (φ \land ψ)) \to (ψ \to φ)$

Metamath Proof Explorer

Theorem mopickr

Proof