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	⊢ ( 𝜑 → 𝐺 = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
	bj-fvsnun2.ex1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	bj-fvsnun2.ex2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	bj-fvsnun2	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bj-fvsnun.un	⊢ ( 𝜑 → 𝐺 = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
2		bj-fvsnun2.ex1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		bj-fvsnun2.ex2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		dmres	⊢ dom ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( ( 𝐶 ∖ { 𝐴 } ) ∩ dom 𝐹 )
5		inss1	⊢ ( ( 𝐶 ∖ { 𝐴 } ) ∩ dom 𝐹 ) ⊆ ( 𝐶 ∖ { 𝐴 } )
6	4 5	eqsstri	⊢ dom ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ⊆ ( 𝐶 ∖ { 𝐴 } )
7	6	a1i	⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ⊆ ( 𝐶 ∖ { 𝐴 } ) )
8		neldifsnd	⊢ ( 𝜑 → ¬ 𝐴 ∈ ( 𝐶 ∖ { 𝐴 } ) )
9	7 8	ssneldd	⊢ ( 𝜑 → ¬ 𝐴 ∈ dom ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
10	1 9 2 3	bj-fununsn2	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝐵 )