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 ( ∃! 𝑥 𝑥 = 𝑥 ↔ ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step Hyp Ref Expression
1 equid 𝑥 = 𝑥
2 1 bitru ( 𝑥 = 𝑥 ↔ ⊤ )
3 2 eubii ( ∃! 𝑥 𝑥 = 𝑥 ↔ ∃! 𝑥 ⊤ )
4 euae ( ∃! 𝑥 ⊤ ↔ ∀ 𝑥 𝑥 = 𝑦 )
5 3 4 bitri ( ∃! 𝑥 𝑥 = 𝑥 ↔ ∀ 𝑥 𝑥 = 𝑦 )