Metamath Proof Explorer


Theorem exists1

Description: Two ways to express "exactly one thing exists". The left-hand side requires only one variable to express this. Both sides are false in set theory, see Theorem dtru . (Contributed by NM, 5-Apr-2004) (Proof shortened by BJ, 7-Oct-2022)

Ref Expression
Assertion exists1 ∃! x x = x x x = y

Proof

Step Hyp Ref Expression
1 equid x = x
2 1 bitru x = x
3 2 eubii ∃! x x = x ∃! x
4 euae ∃! x x x = y
5 3 4 bitri ∃! x x = x x x = y