Theorem setsval

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

	Ref	Expression
Assertion	setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
2		setsvalg	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
3	1 2	mpan2	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
4		dmsnopg	⊢ ( 𝐵 ∈ 𝑊 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
5	4	difeq2d	⊢ ( 𝐵 ∈ 𝑊 → ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( V ∖ { 𝐴 } ) )
6	5	reseq2d	⊢ ( 𝐵 ∈ 𝑊 → ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )
7	6	uneq1d	⊢ ( 𝐵 ∈ 𝑊 → ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
8	3 7	sylan9eq	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )