Metamath Proof Explorer

Theorem 0iun

Description: An empty indexed union is empty. (Contributed by NM, 4-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion 0iun 
|- U_ x e. (/) A = (/)

Proof

Step Hyp Ref Expression
1 rex0 
 |-  -. E. x e. (/) y e. A
2 eliun 
 |-  ( y e. U_ x e. (/) A <-> E. x e. (/) y e. A )
3 1 2 mtbir 
 |-  -. y e. U_ x e. (/) A
4 3 nel0 
 |-  U_ x e. (/) A = (/)