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 A=xAx

Proof

Step Hyp Ref Expression
1 dfuni2 A=y|xAyx
2 df-iun xAx=y|xAyx
3 1 2 eqtr4i A=xAx