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

Proof

Step	Hyp	Ref	Expression
1		iinconst	|- ( A =/= (/) -> |^|_ x e. A (/) = (/) )
2		0ex	|- (/) e. _V
3	2	n0ii	|- -. _V = (/)
4		0iin	|- |^|_ x e. (/) (/) = _V
5	4	eqeq1i	|- ( |^|_ x e. (/) (/) = (/) <-> _V = (/) )
6	3 5	mtbir	|- -. |^|_ x e. (/) (/) = (/)
7		iineq1	|- ( A = (/) -> |^|_ x e. A (/) = |^|_ x e. (/) (/) )
8	7	eqeq1d	|- ( A = (/) -> ( |^|_ x e. A (/) = (/) <-> |^|_ x e. (/) (/) = (/) ) )
9	6 8	mtbiri	|- ( A = (/) -> -. |^|_ x e. A (/) = (/) )
10	9	necon2ai	|- ( |^|_ x e. A (/) = (/) -> A =/= (/) )
11	1 10	impbii	|- ( A =/= (/) <-> |^|_ x e. A (/) = (/) )