Metamath Proof Explorer

Theorem eu6

Description: Alternate definition of the unique existential quantifier df-eu not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993) This used to be the definition of the unique existential quantifier, while df-eu was then proved as dfeu . (Revised by BJ, 30-Sep-2022) (Proof shortened by Wolf Lammen, 3-Jan-2023) Remove use of ax-11 . (Revised by SN, 21-Sep-2023)

Ref Expression
Assertion eu6 ⊢∃!xφ↔∃y∀xφ↔x=y

Proof

Step Hyp Ref Expression
1 dfmoeu ⊢∃xφ→∃y∀xφ↔x=y↔∃y∀xφ→x=y
2 1 anbi2i ⊢∃xφ∧∃xφ→∃y∀xφ↔x=y↔∃xφ∧∃y∀xφ→x=y
3 abai ⊢∃xφ∧∃y∀xφ↔x=y↔∃xφ∧∃xφ→∃y∀xφ↔x=y
4 eu3v ⊢∃!xφ↔∃xφ∧∃y∀xφ→x=y
5 2 3 4 3bitr4ri ⊢∃!xφ↔∃xφ∧∃y∀xφ↔x=y
6 abai ⊢∃y∀xφ↔x=y∧∃xφ↔∃y∀xφ↔x=y∧∃y∀xφ↔x=y→∃xφ
7 ancom ⊢∃xφ∧∃y∀xφ↔x=y↔∃y∀xφ↔x=y∧∃xφ
8 biimpr ⊢φ↔x=y→x=y→φ
9 8 alimi ⊢∀xφ↔x=y→∀xx=y→φ
10 9 eximi ⊢∃y∀xφ↔x=y→∃y∀xx=y→φ
11 exsbim ⊢∃y∀xx=y→φ→∃xφ
12 10 11 syl ⊢∃y∀xφ↔x=y→∃xφ
13 12 biantru ⊢∃y∀xφ↔x=y↔∃y∀xφ↔x=y∧∃y∀xφ↔x=y→∃xφ
14 6 7 13 3bitr4i ⊢∃xφ∧∃y∀xφ↔x=y↔∃y∀xφ↔x=y
15 5 14 bitri ⊢∃!xφ↔∃y∀xφ↔x=y