Metamath Proof Explorer

Theorem eu1

Description: An alternate way to express uniqueness used by some authors. Exercise 2(b) of Margaris p. 110. (Contributed by NM, 20-Aug-1993) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 29-Oct-2018) Avoid ax-13 . (Revised by Wolf Lammen, 7-Feb-2023)

Ref Expression
Hypothesis eu1.nf ⊢ Ⅎ y φ
Assertion eu1 ⊢ ∃! x φ ↔ ∃ x φ ∧ ∀ y y x φ → x = y

Proof

Step Hyp Ref Expression
1 eu1.nf ⊢ Ⅎ y φ
2 nfs1v ⊢ Ⅎ x y x φ
3 2 euf ⊢ ∃! y y x φ ↔ ∃ x ∀ y y x φ ↔ y = x
4 1 sb8euv ⊢ ∃! x φ ↔ ∃! y y x φ
5 1 sb6rfv ⊢ φ ↔ ∀ y y = x → y x φ
6 equcom ⊢ x = y ↔ y = x
7 6 imbi2i ⊢ y x φ → x = y ↔ y x φ → y = x
8 7 albii ⊢ ∀ y y x φ → x = y ↔ ∀ y y x φ → y = x
9 5 8 anbi12ci ⊢ φ ∧ ∀ y y x φ → x = y ↔ ∀ y y x φ → y = x ∧ ∀ y y = x → y x φ
10 albiim ⊢ ∀ y y x φ ↔ y = x ↔ ∀ y y x φ → y = x ∧ ∀ y y = x → y x φ
11 9 10 bitr4i ⊢ φ ∧ ∀ y y x φ → x = y ↔ ∀ y y x φ ↔ y = x
12 11 exbii ⊢ ∃ x φ ∧ ∀ y y x φ → x = y ↔ ∃ x ∀ y y x φ ↔ y = x
13 3 4 12 3bitr4i ⊢ ∃! x φ ↔ ∃ x φ ∧ ∀ y y x φ → x = y