Metamath Proof Explorer


Theorem setsv

Description: The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021)

Ref Expression
Assertion setsv SVBWSsSetABV

Proof

Step Hyp Ref Expression
1 setsval SVBWSsSetAB=SVAAB
2 resexg SVSVAV
3 snex ABV
4 3 a1i SVBWABV
5 unexg SVAVABVSVAABV
6 2 4 5 syl2an2r SVBWSVAABV
7 1 6 eqeltrd SVBWSsSetABV