Theorem setsnid

Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 7-Nov-2024)

	Ref	Expression
Hypotheses	setsid.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	setsnid.n	⊢ ( 𝐸 ‘ ndx ) ≠ 𝐷
Assertion	setsnid	⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		setsid.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
2		setsnid.n	⊢ ( 𝐸 ‘ ndx ) ≠ 𝐷
3		id	⊢ ( 𝑊 ∈ V → 𝑊 ∈ V )
4	1 3	strfvnd	⊢ ( 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
5		ovex	⊢ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ∈ V
6	5 1	strfvn	⊢ ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) )
7		setsres	⊢ ( 𝑊 ∈ V → ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) = ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) )
8	7	fveq1d	⊢ ( 𝑊 ∈ V → ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) )
9		fvex	⊢ ( 𝐸 ‘ ndx ) ∈ V
10		eldifsn	⊢ ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) ↔ ( ( 𝐸 ‘ ndx ) ∈ V ∧ ( 𝐸 ‘ ndx ) ≠ 𝐷 ) )
11	9 2 10	mpbir2an	⊢ ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } )
12		fvres	⊢ ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) → ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) ) )
13	11 12	ax-mp	⊢ ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) )
14		fvres	⊢ ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) → ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
15	11 14	ax-mp	⊢ ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) )
16	8 13 15	3eqtr3g	⊢ ( 𝑊 ∈ V → ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
17	6 16	eqtrid	⊢ ( 𝑊 ∈ V → ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
18	4 17	eqtr4d	⊢ ( 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
19	1	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
20	19	eqcomi	⊢ ( 𝐸 ‘ ∅ ) = ∅
21		eqid	⊢ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) = ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ )
22		reldmsets	⊢ Rel dom sSet
23	20 21 22	oveqprc	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
24	18 23	pm2.61i	⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )