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

Proof

Step	Hyp	Ref	Expression
1		fvsnun.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		fvsnun.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		fvsnun.3	⊢ 𝐺 = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
4	3	reseq1i	⊢ ( 𝐺 ↾ { 𝐴 } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } )
5		resundir	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) )
6		disjdifr	⊢ ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅
7		resdisj	⊢ ( ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) = ∅ )
8	6 7	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) = ∅
9	8	uneq2i	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ∅ )
10		un0	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ∅ ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
11	9 10	eqtri	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
12	5 11	eqtri	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
13	4 12	eqtri	⊢ ( 𝐺 ↾ { 𝐴 } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
14	13	fveq1i	⊢ ( ( 𝐺 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 )
15		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
16	1 15	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
17	16	fvresd	⊢ ( 𝜑 → ( ( 𝐺 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
18	16	fvresd	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) )
19		fvsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )
20	1 2 19	syl2anc	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )
21	18 20	eqtrd	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 ) = 𝐵 )
22	14 17 21	3eqtr3a	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝐵 )