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