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 xA=

Proof

Step Hyp Ref Expression
1 noel ¬y
2 1 a1i xA¬y
3 2 nrex ¬xAy
4 eliun yxAxAy
5 3 4 mtbir ¬yxA
6 5 nel0 xA=