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	|- F = ( x e. D |-> if ( x = Y , X , ( G ` x ) ) )
Assertion	fdmdifeqresdif	|- ( G : ( D \ { Y } ) --> R -> G = ( F |` ( D \ { Y } ) ) )

Proof

Step	Hyp	Ref	Expression
1		fdmdifeqresdif.f	|- F = ( x e. D |-> if ( x = Y , X , ( G ` x ) ) )
2		eldifsnneq	|- ( x e. ( D \ { Y } ) -> -. x = Y )
3	2	adantl	|- ( ( G : ( D \ { Y } ) --> R /\ x e. ( D \ { Y } ) ) -> -. x = Y )
4	3	iffalsed	|- ( ( G : ( D \ { Y } ) --> R /\ x e. ( D \ { Y } ) ) -> if ( x = Y , X , ( G ` x ) ) = ( G ` x ) )
5	4	mpteq2dva	|- ( G : ( D \ { Y } ) --> R -> ( x e. ( D \ { Y } ) |-> if ( x = Y , X , ( G ` x ) ) ) = ( x e. ( D \ { Y } ) |-> ( G ` x ) ) )
6	1	reseq1i	|- ( F |` ( D \ { Y } ) ) = ( ( x e. D |-> if ( x = Y , X , ( G ` x ) ) ) |` ( D \ { Y } ) )
7		difssd	|- ( G : ( D \ { Y } ) --> R -> ( D \ { Y } ) C_ D )
8	7	resmptd	|- ( G : ( D \ { Y } ) --> R -> ( ( x e. D |-> if ( x = Y , X , ( G ` x ) ) ) |` ( D \ { Y } ) ) = ( x e. ( D \ { Y } ) |-> if ( x = Y , X , ( G ` x ) ) ) )
9	6 8	syl5eq	|- ( G : ( D \ { Y } ) --> R -> ( F |` ( D \ { Y } ) ) = ( x e. ( D \ { Y } ) |-> if ( x = Y , X , ( G ` x ) ) ) )
10		ffn	|- ( G : ( D \ { Y } ) --> R -> G Fn ( D \ { Y } ) )
11		dffn5	|- ( G Fn ( D \ { Y } ) <-> G = ( x e. ( D \ { Y } ) |-> ( G ` x ) ) )
12	10 11	sylib	|- ( G : ( D \ { Y } ) --> R -> G = ( x e. ( D \ { Y } ) |-> ( G ` x ) ) )
13	5 9 12	3eqtr4rd	|- ( G : ( D \ { Y } ) --> R -> G = ( F |` ( D \ { Y } ) ) )