Metamath Proof Explorer


Theorem fieq0

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

Proof

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