This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Uniqueness and unique existence Unique existence: the unique existential quantifier exmoeu
Description: Existence is equivalent to uniqueness implying existential uniqueness.
(Contributed by NM , 5-Apr-2004) (Proof shortened by Wolf Lammen , 5-Dec-2018) (Proof shortened by BJ , 7-Oct-2022)
Ref
Expression
Assertion
exmoeu ⊢ ( ∃ 𝑥 𝜑 ↔ ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
Proof
Step
Hyp
Ref
Expression
1
exmoeub ⊢ ( ∃ 𝑥 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )
2
1
biimpd ⊢ ( ∃ 𝑥 𝜑 → ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
3
nexmo ⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 )
4
3
con1i ⊢ ( ¬ ∃* 𝑥 𝜑 → ∃ 𝑥 𝜑 )
5
euex ⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 𝜑 )
6
4 5
ja ⊢ ( ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) → ∃ 𝑥 𝜑 )
7
2 6
impbii ⊢ ( ∃ 𝑥 𝜑 ↔ ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )