Theorem euae

Description: Two ways to express "exactly one thing exists". To paraphrase the statement and explain the label: there Exists a Unique thing if and only if for All x , x Equals some given (and disjoint) y . Both sides are false in set theory, see Theorems neutru and dtru . (Contributed by NM, 5-Apr-2004) State the theorem using truth constant T. . (Revised by BJ, 7-Oct-2022) Reduce axiom dependencies. (Revised by Wolf Lammen, 2-Mar-2023)

	Ref	Expression
Assertion	euae	⊢ ( ∃! 𝑥 ⊤ ↔ ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		extru	⊢ ∃ 𝑥 ⊤
2	1	biantrur	⊢ ( ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) ↔ ( ∃ 𝑥 ⊤ ∧ ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) ) )
3		hbaev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
4	3	19.8w	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
5		hbnaev	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
6		alnex	⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ¬ ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
7	5 6	sylib	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
8	7	con4i	⊢ ( ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 𝑥 = 𝑦 )
9	4 8	impbii	⊢ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
10		trut	⊢ ( 𝑥 = 𝑦 ↔ ( ⊤ → 𝑥 = 𝑦 ) )
11	10	albii	⊢ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
12	11	exbii	⊢ ( ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 ↔ ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
13	9 12	bitri	⊢ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
14		eu3v	⊢ ( ∃! 𝑥 ⊤ ↔ ( ∃ 𝑥 ⊤ ∧ ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) ) )
15	2 13 14	3bitr4ri	⊢ ( ∃! 𝑥 ⊤ ↔ ∀ 𝑥 𝑥 = 𝑦 )