Theorem bj-fvsnun2

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, 18-Mar-2023) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-fvsnun.un	|- ( ph -> G = ( ( F |` ( C \ { A } ) ) u. { <. A , B >. } ) )
	bj-fvsnun2.ex1	|- ( ph -> A e. V )
	bj-fvsnun2.ex2	|- ( ph -> B e. W )
Assertion	bj-fvsnun2	|- ( ph -> ( G ` A ) = B )

Proof

Step	Hyp	Ref	Expression
1		bj-fvsnun.un	|- ( ph -> G = ( ( F |` ( C \ { A } ) ) u. { <. A , B >. } ) )
2		bj-fvsnun2.ex1	|- ( ph -> A e. V )
3		bj-fvsnun2.ex2	|- ( ph -> B e. W )
4		dmres	|- dom ( F |` ( C \ { A } ) ) = ( ( C \ { A } ) i^i dom F )
5		inss1	|- ( ( C \ { A } ) i^i dom F ) C_ ( C \ { A } )
6	4 5	eqsstri	|- dom ( F |` ( C \ { A } ) ) C_ ( C \ { A } )
7	6	a1i	|- ( ph -> dom ( F |` ( C \ { A } ) ) C_ ( C \ { A } ) )
8		neldifsnd	|- ( ph -> -. A e. ( C \ { A } ) )
9	7 8	ssneldd	|- ( ph -> -. A e. dom ( F |` ( C \ { A } ) ) )
10	1 9 2 3	bj-fununsn2	|- ( ph -> ( G ` A ) = B )