Theorem setsvalg

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

	Ref	Expression
Assertion	setsvalg	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
2		elex	⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ V )
3		resexg	⊢ ( 𝑆 ∈ V → ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ V )
4	3	adantr	⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ V )
5		snex	⊢ { 𝐴 } ∈ V
6		unexg	⊢ ( ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ V ∧ { 𝐴 } ∈ V ) → ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ V )
7	4 5 6	sylancl	⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ) → ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ V )
8		simpl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → 𝑠 = 𝑆 )
9		simpr	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → 𝑒 = 𝐴 )
10	9	sneqd	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → { 𝑒 } = { 𝐴 } )
11	10	dmeqd	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → dom { 𝑒 } = dom { 𝐴 } )
12	11	difeq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → ( V ∖ dom { 𝑒 } ) = ( V ∖ dom { 𝐴 } ) )
13	8 12	reseq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) = ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) )
14	13 10	uneq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → ( ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) ∪ { 𝑒 } ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
15		df-sets	⊢ sSet = ( 𝑠 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) ∪ { 𝑒 } ) )
16	14 15	ovmpoga	⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ∧ ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ V ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
17	7 16	mpd3an3	⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
18	1 2 17	syl2an	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )