Theorem euen1b

Description: Two ways to express " A has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Assertion	euen1b	⊢ ( 𝐴 ≈ 1o ↔ ∃! 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		euen1	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ { 𝑥 ∣ 𝑥 ∈ 𝐴 } ≈ 1o )
2		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
3	2	breq1i	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ≈ 1o ↔ 𝐴 ≈ 1o )
4	1 3	bitr2i	⊢ ( 𝐴 ≈ 1o ↔ ∃! 𝑥 𝑥 ∈ 𝐴 )