Description: A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 24-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fieq0 | |- ( A e. V -> ( A = (/) <-> ( fi ` A ) = (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 | |- ( A = (/) -> ( fi ` A ) = ( fi ` (/) ) ) |
|
| 2 | fi0 | |- ( fi ` (/) ) = (/) |
|
| 3 | 1 2 | eqtrdi | |- ( A = (/) -> ( fi ` A ) = (/) ) |
| 4 | ssfii | |- ( A e. V -> A C_ ( fi ` A ) ) |
|
| 5 | sseq0 | |- ( ( A C_ ( fi ` A ) /\ ( fi ` A ) = (/) ) -> A = (/) ) |
|
| 6 | 4 5 | sylan | |- ( ( A e. V /\ ( fi ` A ) = (/) ) -> A = (/) ) |
| 7 | 6 | ex | |- ( A e. V -> ( ( fi ` A ) = (/) -> A = (/) ) ) |
| 8 | 3 7 | impbid2 | |- ( A e. V -> ( A = (/) <-> ( fi ` A ) = (/) ) ) |