Description: The union of a setvar is a set. (Contributed by BJ, 3-May-2021) (Revised by BJ, 6-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | vuniex | |- U. x e. _V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniex2 | |- E. y y = U. x |
|
2 | 1 | issetri | |- U. x e. _V |