Theorem setsvalg

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

	Ref	Expression
Assertion	setsvalg	|- ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( S e. V -> S e. _V )
2		elex	|- ( A e. W -> A e. _V )
3		resexg	|- ( S e. _V -> ( S |` ( _V \ dom { A } ) ) e. _V )
4	3	adantr	|- ( ( S e. _V /\ A e. _V ) -> ( S |` ( _V \ dom { A } ) ) e. _V )
5		snex	|- { A } e. _V
6		unexg	|- ( ( ( S |` ( _V \ dom { A } ) ) e. _V /\ { A } e. _V ) -> ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. _V )
7	4 5 6	sylancl	|- ( ( S e. _V /\ A e. _V ) -> ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. _V )
8		simpl	|- ( ( s = S /\ e = A ) -> s = S )
9		simpr	|- ( ( s = S /\ e = A ) -> e = A )
10	9	sneqd	|- ( ( s = S /\ e = A ) -> { e } = { A } )
11	10	dmeqd	|- ( ( s = S /\ e = A ) -> dom { e } = dom { A } )
12	11	difeq2d	|- ( ( s = S /\ e = A ) -> ( _V \ dom { e } ) = ( _V \ dom { A } ) )
13	8 12	reseq12d	|- ( ( s = S /\ e = A ) -> ( s |` ( _V \ dom { e } ) ) = ( S |` ( _V \ dom { A } ) ) )
14	13 10	uneq12d	|- ( ( s = S /\ e = A ) -> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
15		df-sets	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
16	14 15	ovmpoga	|- ( ( S e. _V /\ A e. _V /\ ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. _V ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
17	7 16	mpd3an3	|- ( ( S e. _V /\ A e. _V ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
18	1 2 17	syl2an	|- ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )