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