This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )