Theorem fmptap

Description: Append an additional value to a function. (Contributed by NM, 6-Jun-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	fmptap.0a	⊢ 𝐴 ∈ V
	fmptap.0b	⊢ 𝐵 ∈ V
	fmptap.1	⊢ ( 𝑅 ∪ { 𝐴 } ) = 𝑆
	fmptap.2	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐵 )
Assertion	fmptap	⊢ ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fmptap.0a	⊢ 𝐴 ∈ V
2		fmptap.0b	⊢ 𝐵 ∈ V
3		fmptap.1	⊢ ( 𝑅 ∪ { 𝐴 } ) = 𝑆
4		fmptap.2	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐵 )
5		fmptsn	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )
6	1 2 5	mp2an	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 )
7		elsni	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
8	7 4	syl	⊢ ( 𝑥 ∈ { 𝐴 } → 𝐶 = 𝐵 )
9	8	mpteq2ia	⊢ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 )
10	6 9	eqtr4i	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 )
11	10	uneq2i	⊢ ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
12		mptun	⊢ ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
13	3	mpteq1i	⊢ ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 )
14	11 12 13	3eqtr2i	⊢ ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 )