Theorem fmptapd

Description: Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017) (Revised by AV, 10-Aug-2024)

	Ref	Expression
Hypotheses	fmptapd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fmptapd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	fmptapd.s	⊢ ( 𝜑 → ( 𝑅 ∪ { 𝐴 } ) = 𝑆 )
	fmptapd.c	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐶 = 𝐵 )
Assertion	fmptapd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fmptapd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		fmptapd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		fmptapd.s	⊢ ( 𝜑 → ( 𝑅 ∪ { 𝐴 } ) = 𝑆 )
4		fmptapd.c	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐶 = 𝐵 )
5	4 1 2	fmptsnd	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
6	5	uneq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) ) )
7		mptun	⊢ ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
8	7	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) ) )
9	3	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) )
10	6 8 9	3eqtr2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) )