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	$$⊢V\in W\to \left(0<\left|V\right|\leftrightarrow \exists xx\in V\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashgt0elex	$$⊢\left(V\in W\wedge 0<\left|V\right|\right)\to \exists xx\in V$$
2		n0	$$⊢V\ne \varnothing \leftrightarrow \exists xx\in V$$
3		hashgt0	$$⊢\left(V\in W\wedge V\ne \varnothing \right)\to 0<\left|V\right|$$
4	2 3	sylan2br	$$⊢\left(V\in W\wedge \exists xx\in V\right)\to 0<\left|V\right|$$
5	1 4	impbida	$$⊢V\in W\to \left(0<\left|V\right|\leftrightarrow \exists xx\in V\right)$$