Description: Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | euen1 | ⊢ ( ∃! 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≈ 1o ) |
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 ) |