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	|- ( E. x e. A B = (/) -> |^|_ x e. A B = (/) )

Proof

Step	Hyp	Ref	Expression
1		nel02	|- ( B = (/) -> -. y e. B )
2	1	reximi	|- ( E. x e. A B = (/) -> E. x e. A -. y e. B )
3		rexnal	|- ( E. x e. A -. y e. B <-> -. A. x e. A y e. B )
4	2 3	sylib	|- ( E. x e. A B = (/) -> -. A. x e. A y e. B )
5		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
6	5	elv	|- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
7	4 6	sylnibr	|- ( E. x e. A B = (/) -> -. y e. |^|_ x e. A B )
8	7	eq0rdv	|- ( E. x e. A B = (/) -> |^|_ x e. A B = (/) )