Metamath Proof Explorer


Theorem setsvalg

Description: Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion setsvalg SVAWSsSetA=SVdomAA

Proof

Step Hyp Ref Expression
1 elex SVSV
2 elex AWAV
3 resexg SVSVdomAV
4 3 adantr SVAVSVdomAV
5 snex AV
6 unexg SVdomAVAVSVdomAAV
7 4 5 6 sylancl SVAVSVdomAAV
8 simpl s=Se=As=S
9 simpr s=Se=Ae=A
10 9 sneqd s=Se=Ae=A
11 10 dmeqd s=Se=Adome=domA
12 11 difeq2d s=Se=AVdome=VdomA
13 8 12 reseq12d s=Se=AsVdome=SVdomA
14 13 10 uneq12d s=Se=AsVdomee=SVdomAA
15 df-sets sSet=sV,eVsVdomee
16 14 15 ovmpoga SVAVSVdomAAVSsSetA=SVdomAA
17 7 16 mpd3an3 SVAVSsSetA=SVdomAA
18 1 2 17 syl2an SVAWSsSetA=SVdomAA