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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = ∅ ↔ ( fi ‘ 𝐴 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐴 = ∅ → ( fi ‘ 𝐴 ) = ( fi ‘ ∅ ) )
2		fi0	⊢ ( fi ‘ ∅ ) = ∅
3	1 2	eqtrdi	⊢ ( 𝐴 = ∅ → ( fi ‘ 𝐴 ) = ∅ )
4		ssfii	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
5		sseq0	⊢ ( ( 𝐴 ⊆ ( fi ‘ 𝐴 ) ∧ ( fi ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
6	4 5	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( fi ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
7	6	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ( fi ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
8	3 7	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = ∅ ↔ ( fi ‘ 𝐴 ) = ∅ ) )