Theorem hashgt0elexb

Description: The size of a set is greater than zero if and only if the set contains at least one element. (Contributed by Alexander van der Vekens, 18-Jan-2018)

	Ref	Expression
Assertion	hashgt0elexb	⊢ ( 𝑉 ∈ 𝑊 → ( 0 < ( ♯ ‘ 𝑉 ) ↔ ∃ 𝑥 𝑥 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		hashgt0elex	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 0 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑥 𝑥 ∈ 𝑉 )
2		n0	⊢ ( 𝑉 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑉 )
3		hashgt0	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → 0 < ( ♯ ‘ 𝑉 ) )
4	2 3	sylan2br	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ∃ 𝑥 𝑥 ∈ 𝑉 ) → 0 < ( ♯ ‘ 𝑉 ) )
5	1 4	impbida	⊢ ( 𝑉 ∈ 𝑊 → ( 0 < ( ♯ ‘ 𝑉 ) ↔ ∃ 𝑥 𝑥 ∈ 𝑉 ) )