Description: Indexed union of a constant class, i.e. where B does not depend on x . (Contributed by NM, 5-Sep-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | iunconst | |- ( A =/= (/) -> U_ x e. A B = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eliun | |- ( y e. U_ x e. A B <-> E. x e. A y e. B ) |
|
| 2 | r19.9rzv | |- ( A =/= (/) -> ( y e. B <-> E. x e. A y e. B ) ) |
|
| 3 | 1 2 | bitr4id | |- ( A =/= (/) -> ( y e. U_ x e. A B <-> y e. B ) ) |
| 4 | 3 | eqrdv | |- ( A =/= (/) -> U_ x e. A B = B ) |