Metamath Proof Explorer

Theorem iun0

Description: An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

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