Theorem fvsetsid

Description: The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018)

	Ref	Expression
Assertion	fvsetsid	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑋 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		setsval	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ 𝑈 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
2	1	3adant2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
3	2	fveq1d	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑋 ) = ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
4		simp2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝑊 )
5		simp3	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
6		neldifsn	⊢ ¬ 𝑋 ∈ ( V ∖ { 𝑋 } )
7		dmres	⊢ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( ( V ∖ { 𝑋 } ) ∩ dom 𝐹 )
8		inss1	⊢ ( ( V ∖ { 𝑋 } ) ∩ dom 𝐹 ) ⊆ ( V ∖ { 𝑋 } )
9	7 8	eqsstri	⊢ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ⊆ ( V ∖ { 𝑋 } )
10	9	sseli	⊢ ( 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) → 𝑋 ∈ ( V ∖ { 𝑋 } ) )
11	6 10	mto	⊢ ¬ 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) )
12	11	a1i	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ¬ 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) )
13		fsnunfv	⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ∧ ¬ 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ) → ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
14	4 5 12 13	syl3anc	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
15	3 14	eqtrd	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑋 ) = 𝑌 )