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		incom	⊢ ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ( { 𝐴 } ∩ ( 𝐶 ∖ { 𝐴 } ) )
7		disjdif	⊢ ( { 𝐴 } ∩ ( 𝐶 ∖ { 𝐴 } ) ) = ∅
8	6 7	eqtri	⊢ ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅
9		resdisj	⊢ ( ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) = ∅ )
10	8 9	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) = ∅
11	10	uneq2i	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ∅ )
12		un0	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ∅ ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
13	11 12	eqtri	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
14	5 13	eqtri	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
15	4 14	eqtri	⊢ ( 𝐺 ↾ { 𝐴 } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
16	15	fveq1i	⊢ ( ( 𝐺 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 )
17		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
18	1 17	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
19	18	fvresd	⊢ ( 𝜑 → ( ( 𝐺 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
20	18	fvresd	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) )
21		fvsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )
22	1 2 21	syl2anc	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )
23	20 22	eqtrd	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 ) = 𝐵 )
24	16 19 23	3eqtr3a	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝐵 )