Theorem fvsnun1

Description: The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 . (Contributed by NM, 23-Sep-2007) Put in deduction form. (Revised by BJ, 25-Feb-2023)

	Ref	Expression
Hypotheses	fvsnun.1	|- ( ph -> A e. V )
	fvsnun.2	|- ( ph -> B e. W )
	fvsnun.3	|- G = ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) )
Assertion	fvsnun1	|- ( ph -> ( G ` A ) = B )

Proof

Step	Hyp	Ref	Expression
1		fvsnun.1	|- ( ph -> A e. V )
2		fvsnun.2	|- ( ph -> B e. W )
3		fvsnun.3	|- G = ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) )
4	3	reseq1i	|- ( G |` { A } ) = ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` { A } )
5		resundir	|- ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` { A } ) = ( ( { <. A , B >. } |` { A } ) u. ( ( F |` ( C \ { A } ) ) |` { A } ) )
6		incom	|- ( ( C \ { A } ) i^i { A } ) = ( { A } i^i ( C \ { A } ) )
7		disjdif	|- ( { A } i^i ( C \ { A } ) ) = (/)
8	6 7	eqtri	|- ( ( C \ { A } ) i^i { A } ) = (/)
9		resdisj	|- ( ( ( C \ { A } ) i^i { A } ) = (/) -> ( ( F |` ( C \ { A } ) ) |` { A } ) = (/) )
10	8 9	ax-mp	|- ( ( F |` ( C \ { A } ) ) |` { A } ) = (/)
11	10	uneq2i	|- ( ( { <. A , B >. } |` { A } ) u. ( ( F |` ( C \ { A } ) ) |` { A } ) ) = ( ( { <. A , B >. } |` { A } ) u. (/) )
12		un0	|- ( ( { <. A , B >. } |` { A } ) u. (/) ) = ( { <. A , B >. } |` { A } )
13	11 12	eqtri	|- ( ( { <. A , B >. } |` { A } ) u. ( ( F |` ( C \ { A } ) ) |` { A } ) ) = ( { <. A , B >. } |` { A } )
14	5 13	eqtri	|- ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` { A } ) = ( { <. A , B >. } |` { A } )
15	4 14	eqtri	|- ( G |` { A } ) = ( { <. A , B >. } |` { A } )
16	15	fveq1i	|- ( ( G |` { A } ) ` A ) = ( ( { <. A , B >. } |` { A } ) ` A )
17		snidg	|- ( A e. V -> A e. { A } )
18	1 17	syl	|- ( ph -> A e. { A } )
19	18	fvresd	|- ( ph -> ( ( G |` { A } ) ` A ) = ( G ` A ) )
20	18	fvresd	|- ( ph -> ( ( { <. A , B >. } |` { A } ) ` A ) = ( { <. A , B >. } ` A ) )
21		fvsng	|- ( ( A e. V /\ B e. W ) -> ( { <. A , B >. } ` A ) = B )
22	1 2 21	syl2anc	|- ( ph -> ( { <. A , B >. } ` A ) = B )
23	20 22	eqtrd	|- ( ph -> ( ( { <. A , B >. } |` { A } ) ` A ) = B )
24	16 19 23	3eqtr3a	|- ( ph -> ( G ` A ) = B )