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 =/= (/) ) |
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 =/= (/) ) |