Metamath Proof Explorer

Theorem wl-euae

Description: Two ways to express "exactly one thing exists" . (Contributed by Wolf Lammen, 5-Mar-2023)

Ref Expression
Assertion wl-euae ⊢ ∃! x ⊤ ↔ ∀ x x = y

Proof

Step Hyp Ref Expression
1 df-eu ⊢ ∃! x ⊤ ↔ ∃ x ⊤ ∧ ∃* x ⊤
2 extru ⊢ ∃ x ⊤
3 2 biantrur ⊢ ∃* x ⊤ ↔ ∃ x ⊤ ∧ ∃* x ⊤
4 wl-moae ⊢ ∃* x ⊤ ↔ ∀ x x = y
5 1 3 4 3bitr2i ⊢ ∃! x ⊤ ↔ ∀ x x = y