This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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