Theorem fdmdifeqresdif

Description: The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019)

	Ref	Expression
Hypothesis	fdmdifeqresdif.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) )
Assertion	fdmdifeqresdif	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → 𝐺 = ( 𝐹 ↾ ( 𝐷 ∖ { 𝑌 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		fdmdifeqresdif.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) )
2		eldifsnneq	⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) → ¬ 𝑥 = 𝑌 )
3	2	adantl	⊢ ( ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 ∧ 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ) → ¬ 𝑥 = 𝑌 )
4	3	iffalsed	⊢ ( ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 ∧ 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ) → if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
5	4	mpteq2dva	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
6	1	reseq1i	⊢ ( 𝐹 ↾ ( 𝐷 ∖ { 𝑌 } ) ) = ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) ) ↾ ( 𝐷 ∖ { 𝑌 } ) )
7		difssd	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → ( 𝐷 ∖ { 𝑌 } ) ⊆ 𝐷 )
8	7	resmptd	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) ) ↾ ( 𝐷 ∖ { 𝑌 } ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) ) )
9	6 8	syl5eq	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → ( 𝐹 ↾ ( 𝐷 ∖ { 𝑌 } ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ↦ if ( 𝑥 = 𝑌 , 𝑋 , ( 𝐺 ‘ 𝑥 ) ) ) )
10		ffn	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → 𝐺 Fn ( 𝐷 ∖ { 𝑌 } ) )
11		dffn5	⊢ ( 𝐺 Fn ( 𝐷 ∖ { 𝑌 } ) ↔ 𝐺 = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
12	10 11	sylib	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → 𝐺 = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑌 } ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
13	5 9 12	3eqtr4rd	⊢ ( 𝐺 : ( 𝐷 ∖ { 𝑌 } ) ⟶ 𝑅 → 𝐺 = ( 𝐹 ↾ ( 𝐷 ∖ { 𝑌 } ) ) )