Metamath Proof Explorer


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 )