Theorem wl-moae

Description: Two ways to express "at most one thing exists" or, in this context equivalently, "exactly one thing exists" . The equivalence results from the presence of ax-6 in the proof, that ensures "at least one thing exists". For other equivalences see wl-euae and exists1 . Gerard Lang pointed out, that E. y A. x x = y with disjoint x and y ( df-mo , trut ) also means "exactly one thing exists" . (Contributed by NM, 5-Apr-2004) State the theorem using truth constant T. . (Revised by BJ, 7-Oct-2022) Reduce axiom dependencies, and use E* . (Revised by Wolf Lammen, 7-Mar-2023)

	Ref	Expression
Assertion	wl-moae	⊢ ( ∃* 𝑥 ⊤ ↔ ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		wl-motae	⊢ ( ∃* 𝑥 ⊤ → ∀ 𝑥 𝑥 = 𝑦 )
2		hbaev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
3	2	19.8w	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
4		ax-1	⊢ ( 𝑥 = 𝑦 → ( ⊤ → 𝑥 = 𝑦 ) )
5	4	alimi	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
6	5	eximi	⊢ ( ∃ 𝑦 ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
7	3 6	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
8		df-mo	⊢ ( ∃* 𝑥 ⊤ ↔ ∃ 𝑦 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑦 ) )
9	7 8	sylibr	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃* 𝑥 ⊤ )
10	1 9	impbii	⊢ ( ∃* 𝑥 ⊤ ↔ ∀ 𝑥 𝑥 = 𝑦 )