Metamath Proof Explorer

Theorem uniiun

Description: Class union in terms of indexed union. Definition in Stoll p. 43. (Contributed by NM, 28-Jun-1998)

Ref Expression
Assertion uniiun 
|- U. A = U_ x e. A x

Proof

Step Hyp Ref Expression
1 dfuni2 
 |-  U. A = { y | E. x e. A y e. x }
2 df-iun 
 |-  U_ x e. A x = { y | E. x e. A y e. x }
3 1 2 eqtr4i 
 |-  U. A = U_ x e. A x