Theorem iineq0

Description: An indexed intersection is empty if one of the intersected classes is empty. (Contributed by Zhi Wang, 30-Oct-2025)

	Ref	Expression
Assertion	iineq0	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		nel02	⊢ ( 𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵 )
2	1	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → ∃ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐵 )
3		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑦 ∈ 𝐵 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
4	2 3	sylib	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → ¬ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
6	5	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
7	4 6	sylnibr	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → ¬ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 )
8	7	eq0rdv	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = ∅ )