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 } |
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 } |