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	biimtrdi	|- ( A e. V -> ( ( # ` A ) = 1 -> A =/= (/) ) )
9	8	imp	|- ( ( A e. V /\ ( # ` A ) = 1 ) -> A =/= (/) )