Description: The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | setsv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | setsval | |
|
2 | resexg | |
|
3 | snex | |
|
4 | 3 | a1i | |
5 | unexg | |
|
6 | 2 4 5 | syl2an2r | |
7 | 1 6 | eqeltrd | |