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

Metamath Proof Explorer

Theorem eupick

Description: Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing x such that ph is true, and there is also an x (actually the same one) such that ph and ps are both true, then ph implies ps regardless of x . This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in WhiteheadRussell p. 192. (Contributed by NM, 10-Jul-1994)

		Ref	Expression
	Assertion	eupick	⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		eumo	⊢ ( ∃! 𝑥 𝜑 → ∃* 𝑥 𝜑 )
2		mopick	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )
3	1 2	sylan	⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )