Theorem eqeuel

Description: A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022)

	Ref	Expression
Assertion	eqeuel	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) → ∃! 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
2	1	biimpi	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐴 )
3	2	anim1i	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) → ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) )
4		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
5	4	eu4	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) )
6	3 5	sylibr	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) → ∃! 𝑥 𝑥 ∈ 𝐴 )