Metamath Proof Explorer


Theorem hash1n0

Description: If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020)

Ref Expression
Assertion hash1n0
|- ( ( A e. V /\ ( # ` A ) = 1 ) -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 hash1snb
 |-  ( A e. V -> ( ( # ` A ) = 1 <-> E. a A = { a } ) )
2 id
 |-  ( A = { a } -> A = { a } )
3 vex
 |-  a e. _V
4 3 snnz
 |-  { a } =/= (/)
5 4 a1i
 |-  ( A = { a } -> { a } =/= (/) )
6 2 5 eqnetrd
 |-  ( A = { a } -> A =/= (/) )
7 6 exlimiv
 |-  ( E. a A = { a } -> A =/= (/) )
8 1 7 syl6bi
 |-  ( A e. V -> ( ( # ` A ) = 1 -> A =/= (/) ) )
9 8 imp
 |-  ( ( A e. V /\ ( # ` A ) = 1 ) -> A =/= (/) )