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 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 V A fi A
5 sseq0 A fi A fi A = A =
6 4 5 sylan A V fi A = A =
7 6 ex A V fi A = A =
8 3 7 impbid2 A V A = fi A =