Description: The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | euhash1 | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃! 𝑎 𝑎 ∈ 𝑉 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashen1 | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 1 ↔ 𝑉 ≈ 1o ) ) | |
2 | euen1b | ⊢ ( 𝑉 ≈ 1o ↔ ∃! 𝑎 𝑎 ∈ 𝑉 ) | |
3 | 1 2 | bitrdi | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃! 𝑎 𝑎 ∈ 𝑉 ) ) |