Metamath Proof Explorer

Theorem hashgt0n0

Description: If the size of a set is greater than 0, the set is not empty. (Contributed by AV, 5-Aug-2018) (Proof shortened by AV, 18-Nov-2018)

Ref Expression
Assertion hashgt0n0 
|- ( ( A e. V /\ 0 < ( # ` A ) ) -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 hashneq0 
 |-  ( A e. V -> ( 0 < ( # ` A ) <-> A =/= (/) ) )
2 1 biimpa 
 |-  ( ( A e. V /\ 0 < ( # ` A ) ) -> A =/= (/) )