Theorem iin0

Description: An indexed intersection of the empty set, with a nonempty index set, is empty. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	iin0	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝑥 ∈ 𝐴 ∅ = ∅ )

Proof

Step	Hyp	Ref	Expression
1		iinconst	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ∅ = ∅ )
2		0ex	⊢ ∅ ∈ V
3	2	n0ii	⊢ ¬ V = ∅
4		0iin	⊢ ∩ 𝑥 ∈ ∅ ∅ = V
5	4	eqeq1i	⊢ ( ∩ 𝑥 ∈ ∅ ∅ = ∅ ↔ V = ∅ )
6	3 5	mtbir	⊢ ¬ ∩ 𝑥 ∈ ∅ ∅ = ∅
7		iineq1	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ∅ = ∩ 𝑥 ∈ ∅ ∅ )
8	7	eqeq1d	⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 ∅ = ∅ ↔ ∩ 𝑥 ∈ ∅ ∅ = ∅ ) )
9	6 8	mtbiri	⊢ ( 𝐴 = ∅ → ¬ ∩ 𝑥 ∈ 𝐴 ∅ = ∅ )
10	9	necon2ai	⊢ ( ∩ 𝑥 ∈ 𝐴 ∅ = ∅ → 𝐴 ≠ ∅ )
11	1 10	impbii	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝑥 ∈ 𝐴 ∅ = ∅ )