Description: The output of the collection operation is a set if the second input is. (Contributed by Rohan Ridenour, 11-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | collexd.1 | ||
Assertion | collexd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | collexd.1 | ||
2 | df-coll | ||
3 | scottex2 | ||
4 | 3 | a1i | |
5 | 4 | ralrimivw | |
6 | iunexg | ||
7 | 1 5 6 | syl2anc | |
8 | 2 7 | eqeltrid |