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\in V\to \left(A=\varnothing \leftrightarrow \mathrm{fi}\left(A\right)=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=\varnothing \to \mathrm{fi}\left(A\right)=\mathrm{fi}\left(\varnothing \right)$$
2		fi0	$$⊢\mathrm{fi}\left(\varnothing \right)=\varnothing$$
3	1 2	eqtrdi	$$⊢A=\varnothing \to \mathrm{fi}\left(A\right)=\varnothing$$
4		ssfii	$$⊢A\in V\to A\subseteq \mathrm{fi}\left(A\right)$$
5		sseq0	$$⊢\left(A\subseteq \mathrm{fi}\left(A\right)\wedge \mathrm{fi}\left(A\right)=\varnothing \right)\to A=\varnothing$$
6	4 5	sylan	$$⊢\left(A\in V\wedge \mathrm{fi}\left(A\right)=\varnothing \right)\to A=\varnothing$$
7	6	ex	$$⊢A\in V\to \left(\mathrm{fi}\left(A\right)=\varnothing \to A=\varnothing \right)$$
8	3 7	impbid2	$$⊢A\in V\to \left(A=\varnothing \leftrightarrow \mathrm{fi}\left(A\right)=\varnothing \right)$$