Metamath Proof Explorer


Theorem iunsn

Description: Indexed union of a singleton. Compare dfiun2 and rnmpt . (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Assertion iunsn
|- U_ x e. A { B } = { y | E. x e. A y = B }

Proof

Step Hyp Ref Expression
1 df-iun
 |-  U_ x e. A { B } = { y | E. x e. A y e. { B } }
2 velsn
 |-  ( y e. { B } <-> y = B )
3 2 rexbii
 |-  ( E. x e. A y e. { B } <-> E. x e. A y = B )
4 3 abbii
 |-  { y | E. x e. A y e. { B } } = { y | E. x e. A y = B }
5 1 4 eqtri
 |-  U_ x e. A { B } = { y | E. x e. A y = B }