This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (/) = (/) )