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 → ∀ x x = y → φ
10 9 eximi ⊢ ∃ y ∀ x φ ↔ x = y → ∃ y ∀ x x = y → φ
11 exsbim ⊢ ∃ y ∀ x x = 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