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	$⊢ (S \in V \land B \in W) \to S sSet ⟨A, B⟩ = ({S ↾}_{(V ∖ \{A\})}) \cup \{⟨A, B⟩\}$

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨A, B⟩ \in V$
2		setsvalg	$⊢ (S \in V \land ⟨A, B⟩ \in V) \to S sSet ⟨A, B⟩ = ({S ↾}_{(V ∖ dom \{⟨A, B⟩\})}) \cup \{⟨A, B⟩\}$
3	1 2	mpan2	$⊢ S \in V \to S sSet ⟨A, B⟩ = ({S ↾}_{(V ∖ dom \{⟨A, B⟩\})}) \cup \{⟨A, B⟩\}$
4		dmsnopg	$⊢ B \in W \to dom \{⟨A, B⟩\} = \{A\}$
5	4	difeq2d	$⊢ B \in W \to V ∖ dom \{⟨A, B⟩\} = V ∖ \{A\}$
6	5	reseq2d	$⊢ B \in W \to {S ↾}_{(V ∖ dom \{⟨A, B⟩\})} = {S ↾}_{(V ∖ \{A\})}$
7	6	uneq1d	$⊢ B \in W \to ({S ↾}_{(V ∖ dom \{⟨A, B⟩\})}) \cup \{⟨A, B⟩\} = ({S ↾}_{(V ∖ \{A\})}) \cup \{⟨A, B⟩\}$
8	3 7	sylan9eq	$⊢ (S \in V \land B \in W) \to S sSet ⟨A, B⟩ = ({S ↾}_{(V ∖ \{A\})}) \cup \{⟨A, B⟩\}$

Metamath Proof Explorer