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

Metamath Proof Explorer

Theorem moeu

Description: Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995) This used to be the definition of the at-most-one quantifier, while df-mo was then proved as dfmo . (Revised by BJ, 30-Sep-2022)

		Ref	Expression
	Assertion	moeu	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		moabs	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 ) )
2		exmoeub	⊢ ( ∃ 𝑥 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )
3	2	pm5.74i	⊢ ( ( ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
4	1 3	bitri	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )