Theorem reuen1

Description: Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	reuen1	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≈ 1o )

Proof

Step	Hyp	Ref	Expression
1		reusn	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 } )
2		en1	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≈ 1o ↔ ∃ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 } )
3	1 2	bitr4i	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≈ 1o )