Theorem euequ

Description: There exists a unique set equal to a given set. Special case of eueqi proved using only predicate calculus. The proof needs y = z be free of x . This is ensured by having x and y be distinct. Alternately, a distinctor -. A. x x = y could have been used instead. See eueq and eueqi for classes. (Contributed by Stefan Allan, 4-Dec-2008) (Proof shortened by Wolf Lammen, 8-Sep-2019) Reduce axiom usage. (Revised by Wolf Lammen, 1-Mar-2023)

	Ref	Expression
Assertion	euequ	⊢ ∃! 𝑥 𝑥 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑦
2		ax6ev	⊢ ∃ 𝑧 𝑧 = 𝑦
3		equeuclr	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) )
4	3	alrimiv	⊢ ( 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) )
5	2 4	eximii	⊢ ∃ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 )
6		eu3v	⊢ ( ∃! 𝑥 𝑥 = 𝑦 ↔ ( ∃ 𝑥 𝑥 = 𝑦 ∧ ∃ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) ) )
7	1 5 6	mpbir2an	⊢ ∃! 𝑥 𝑥 = 𝑦