Theorem euen1

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

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

Proof

Step	Hyp	Ref	Expression
1		reuen1	⊢ ( ∃! 𝑥 ∈ V 𝜑 ↔ { 𝑥 ∈ V ∣ 𝜑 } ≈ 1o )
2		reuv	⊢ ( ∃! 𝑥 ∈ V 𝜑 ↔ ∃! 𝑥 𝜑 )
3		rabab	⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ 𝜑 }
4	3	breq1i	⊢ ( { 𝑥 ∈ V ∣ 𝜑 } ≈ 1o ↔ { 𝑥 ∣ 𝜑 } ≈ 1o )
5	1 2 4	3bitr3i	⊢ ( ∃! 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≈ 1o )